Theorem chj1i

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

	Ref	Expression
Hypothesis	ch0le.1	|- A e. CH
Assertion	chj1i	|- ( A vH ~H ) = ~H

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	|- A e. CH
2		helch	|- ~H e. CH
3	1 2	chjcli	|- ( A vH ~H ) e. CH
4	3	chssii	|- ( A vH ~H ) C_ ~H
5	2 1	chub2i	|- ~H C_ ( A vH ~H )
6	4 5	eqssi	|- ( A vH ~H ) = ~H