Metamath Proof Explorer


Theorem ollat

Description: An ortholattice is a lattice. (Contributed by NM, 18-Sep-2011)

Ref Expression
Assertion ollat
|- ( K e. OL -> K e. Lat )

Proof

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