Metamath Proof Explorer

Theorem pjococi

Description: Proof of orthocomplement theorem using projections. Compare ococ . (Contributed by NM, 5-Nov-1999) (New usage is discouraged.)

Ref Expression
Hypothesis pjococ.1 
|- H e. CH
Assertion pjococi 
|- ( _|_ ` ( _|_ ` H ) ) = H

Proof

Step Hyp Ref Expression
1 pjococ.1 
 |-  H e. CH
2 1 ococi 
 |-  ( _|_ ` ( _|_ ` H ) ) = H