Metamath Proof Explorer

Theorem choccli

Description: Closure of CH orthocomplement. (Contributed by NM, 29-Jul-1999) (New usage is discouraged.)

Ref Expression
Hypothesis choccl.1 
|- A e. CH
Assertion choccli 
|- ( _|_ ` A ) e. CH

Proof

Step Hyp Ref Expression
1 choccl.1 
 |-  A e. CH
2 choccl 
 |-  ( A e. CH -> ( _|_ ` A ) e. CH )
3 1 2 ax-mp 
 |-  ( _|_ ` A ) e. CH