Description: Define the class of ortholattices. Definition from Kalmbach p. 16. (Contributed by NM, 18-Sep-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | df-ol | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | col | |
|
1 | clat | |
|
2 | cops | |
|
3 | 1 2 | cin | |
4 | 0 3 | wceq | |