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