Metamath Proof Explorer


Theorem shub2

Description: A subspace is a subset of its Hilbert lattice join with another. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion shub2 A S B S A B A

Proof

Step Hyp Ref Expression
1 shub1 A S B S A A B
2 shjcom A S B S A B = B A
3 1 2 sseqtrd A S B S A B A