Description: A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | hlcvl | ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CvLat ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlomcmcv | ⊢ ( 𝐾 ∈ HL → ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ) | |
2 | 1 | simp3d | ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CvLat ) |