Metamath Proof Explorer


Theorem olposN

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

Ref Expression
Assertion olposN K OL K Poset

Proof

Step Hyp Ref Expression
1 olop K OL K OP
2 opposet K OP K Poset
3 1 2 syl K OL K Poset