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	$$⊢\mathrm{OL}=\mathrm{Lat}\cap \mathrm{OP}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		col	$$class\mathrm{OL}$$
1		clat	$$class\mathrm{Lat}$$
2		cops	$$class\mathrm{OP}$$
3	1 2	cin	$$class\left(\mathrm{Lat}\cap \mathrm{OP}\right)$$
4	0 3	wceq	$$wff\mathrm{OL}=\mathrm{Lat}\cap \mathrm{OP}$$