Description: A Hilbert lattice is orthomodular. (Contributed by NM, 20-Oct-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | hloml | ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OML ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlomcmcv | ⊢ ( 𝐾 ∈ HL → ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ) | |
2 | 1 | simp1d | ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OML ) |