Metamath Proof Explorer


Theorem isolat

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

Ref Expression
Assertion isolat K OL K Lat K OP

Proof

Step Hyp Ref Expression
1 df-ol OL = Lat OP
2 1 elin2 K OL K Lat K OP