Theorem olposN

Description: An ortholattice is a poset. (Contributed by NM, 16-Oct-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	olposN	$$⊢K\in \mathrm{OL}\to K\in \mathrm{Poset}$$

Proof

Step	Hyp	Ref	Expression
1		olop	$$⊢K\in \mathrm{OL}\to K\in \mathrm{OP}$$
2		opposet	$$⊢K\in \mathrm{OP}\to K\in \mathrm{Poset}$$
3	1 2	syl	$$⊢K\in \mathrm{OL}\to K\in \mathrm{Poset}$$