Theorem olposN

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

	Ref	Expression
Assertion	olposN	⊢ ( 𝐾 ∈ OL → 𝐾 ∈ Poset )

Proof

Step	Hyp	Ref	Expression
1		olop	⊢ ( 𝐾 ∈ OL → 𝐾 ∈ OP )
2		opposet	⊢ ( 𝐾 ∈ OP → 𝐾 ∈ Poset )
3	1 2	syl	⊢ ( 𝐾 ∈ OL → 𝐾 ∈ Poset )