Theorem qlax1i

Description: One of the equations showing CH is an ortholattice. (This corresponds to axiom "ax-1" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004) (New usage is discouraged.)

	Ref	Expression
Hypothesis	qlax1.1	⊢ 𝐴 ∈ Cℋ
Assertion	qlax1i	⊢ 𝐴 = ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		qlax1.1	⊢ 𝐴 ∈ Cℋ
2	1	ococi	⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴
3	2	eqcomi	⊢ 𝐴 = ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) )