Description: An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | olop | ⊢ ( 𝐾 ∈ OL → 𝐾 ∈ OP ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isolat | ⊢ ( 𝐾 ∈ OL ↔ ( 𝐾 ∈ Lat ∧ 𝐾 ∈ OP ) ) | |
2 | 1 | simprbi | ⊢ ( 𝐾 ∈ OL → 𝐾 ∈ OP ) |