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 e. OL -> K e. Poset )

Proof

Step Hyp Ref Expression
1 olop 
 |-  ( K e. OL -> K e. OP )
2 opposet 
 |-  ( K e. OP -> K e. Poset )
3 1 2 syl 
 |-  ( K e. OL -> K e. Poset )