Metamath Proof Explorer

Theorem isolat

Description: The predicate "is an ortholattice." (Contributed by NM, 18-Sep-2011)

Ref Expression
Assertion isolat 
|- ( K e. OL <-> ( K e. Lat /\ K e. OP ) )

Proof

Step Hyp Ref Expression
1 df-ol 
 |-  OL = ( Lat i^i OP )
2 1 elin2 
 |-  ( K e. OL <-> ( K e. Lat /\ K e. OP ) )