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 i^i OP )

Detailed syntax breakdown

Step Hyp Ref Expression
0 col 
 |-  OL
1 clat 
 |-  Lat
2 cops 
 |-  OP
3 1 2 cin 
 |-  ( Lat i^i OP )
4 0 3 wceq 
 |-  OL = ( Lat i^i OP )