Theorem mdoc2i

Description: Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	mdoc1.1	⊢ 𝐴 ∈ Cℋ
Assertion	mdoc2i	⊢ ( ⊥ ‘ 𝐴 ) 𝑀ℋ 𝐴

Proof

Step	Hyp	Ref	Expression
1		mdoc1.1	⊢ 𝐴 ∈ Cℋ
2	1	choccli	⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
3	2	mdoc1i	⊢ ( ⊥ ‘ 𝐴 ) 𝑀ℋ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) )
4	1	ococi	⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴
5	3 4	breqtri	⊢ ( ⊥ ‘ 𝐴 ) 𝑀ℋ 𝐴