Theorem mdoc2i

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

	Ref	Expression
Hypothesis	mdoc1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	mdoc2i	$$⊢\perp \left(A\right){𝑀}_{\mathscr{H}}A$$

Proof

Step	Hyp	Ref	Expression
1		mdoc1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	choccli	$$⊢\perp \left(A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
3	2	mdoc1i	$$⊢\perp \left(A\right){𝑀}_{\mathscr{H}}\perp \left(\perp \left(A\right)\right)$$
4	1	ococi	$$⊢\perp \left(\perp \left(A\right)\right)=A$$
5	3 4	breqtri	$$⊢\perp \left(A\right){𝑀}_{\mathscr{H}}A$$