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	⊢ OL
1		clat	⊢ Lat
2		cops	⊢ OP
3	1 2	cin	⊢ ( Lat ∩ OP )
4	0 3	wceq	⊢ OL = ( Lat ∩ OP )