Metamath Proof Explorer


Theorem olop

Description: An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011)

Ref Expression
Assertion olop KOLKOP

Proof

Step Hyp Ref Expression
1 isolat KOLKLatKOP
2 1 simprbi KOLKOP