Metamath Proof Explorer

Theorem isolatiN

Description: Properties that determine an ortholattice. (Contributed by NM, 18-Sep-2011) (New usage is discouraged.)

Ref Expression
Hypotheses isolati.1 
|- K e. Lat
isolati.2 
|- K e. OP
Assertion isolatiN 
|- K e. OL

Proof

Step Hyp Ref Expression
1 isolati.1 
 |-  K e. Lat
2 isolati.2 
 |-  K e. OP
3 isolat 
 |-  ( K e. OL <-> ( K e. Lat /\ K e. OP ) )
4 1 2 3 mpbir2an 
 |-  K e. OL