Metamath Proof Explorer

Definition df-ol

Description: Define the class of ortholattices. Definition from Kalmbach p. 16. (Contributed by NM, 18-Sep-2011)

Ref Expression
Assertion df-ol OL = Lat OP

Detailed syntax breakdown

Step Hyp Ref Expression
0 col class OL
1 clat class Lat
2 cops class OP
3 1 2 cin class Lat OP
4 0 3 wceq wff OL = Lat OP