Metamath Proof Explorer

Theorem hlomcmat

Description: A Hilbert lattice is orthomodular, complete, and atomic. (Contributed by NM, 5-Nov-2012)

Ref Expression
Assertion hlomcmat ⊢ K ∈ HL → K ∈ OML ∧ K ∈ CLat ∧ K ∈ AtLat

Proof

Step Hyp Ref Expression
1 hloml ⊢ K ∈ HL → K ∈ OML
2 hlclat ⊢ K ∈ HL → K ∈ CLat
3 hlatl ⊢ K ∈ HL → K ∈ AtLat
4 1 2 3 3jca ⊢ K ∈ HL → K ∈ OML ∧ K ∈ CLat ∧ K ∈ AtLat