Metamath Proof Explorer

Theorem shub1

Description: Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion shub1 
|- ( ( A e. SH /\ B e. SH ) -> A C_ ( A vH B ) )

Proof

Step Hyp Ref Expression
1 shsub1 
 |-  ( ( A e. SH /\ B e. SH ) -> A C_ ( A +H B ) )
2 shslej 
 |-  ( ( A e. SH /\ B e. SH ) -> ( A +H B ) C_ ( A vH B ) )
3 1 2 sstrd 
 |-  ( ( A e. SH /\ B e. SH ) -> A C_ ( A vH B ) )