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=LatOP

Detailed syntax breakdown

Step Hyp Ref Expression
0 col classOL
1 clat classLat
2 cops classOP
3 1 2 cin classLatOP
4 0 3 wceq wffOL=LatOP