Theorem shub1i

Description: Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shincl.1	|- A e. SH
	shincl.2	|- B e. SH
Assertion	shub1i	|- A C_ ( A vH B )

Proof

Step	Hyp	Ref	Expression
1		shincl.1	|- A e. SH
2		shincl.2	|- B e. SH
3	1 2	shsub1i	|- A C_ ( A +H B )
4	1 2	shsleji	|- ( A +H B ) C_ ( A vH B )
5	3 4	sstri	|- A C_ ( A vH B )