Theorem chj1i

Description: Join with Hilbert lattice one. (Contributed by NM, 6-Aug-2004) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ch0le.1	⊢ 𝐴 ∈ Cℋ
Assertion	chj1i	⊢ ( 𝐴 ∨ℋ ℋ ) = ℋ

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	⊢ 𝐴 ∈ Cℋ
2		helch	⊢ ℋ ∈ Cℋ
3	1 2	chjcli	⊢ ( 𝐴 ∨ℋ ℋ ) ∈ Cℋ
4	3	chssii	⊢ ( 𝐴 ∨ℋ ℋ ) ⊆ ℋ
5	2 1	chub2i	⊢ ℋ ⊆ ( 𝐴 ∨ℋ ℋ )
6	4 5	eqssi	⊢ ( 𝐴 ∨ℋ ℋ ) = ℋ