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	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	qlax1i	$$⊢A=\perp \left(\perp \left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		qlax1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	ococi	$$⊢\perp \left(\perp \left(A\right)\right)=A$$
3	2	eqcomi	$$⊢A=\perp \left(\perp \left(A\right)\right)$$