This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isolat

Description: The predicate "is an ortholattice." (Contributed by NM, 18-Sep-2011)

Ref Expression
Assertion isolat ⊢ K ∈ OL ↔ K ∈ Lat ∧ K ∈ OP

Proof

Step Hyp Ref Expression
1 df-ol ⊢ OL = Lat ∩ OP
2 1 elin2 ⊢ K ∈ OL ↔ K ∈ Lat ∧ K ∈ OP