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 e. HL -> ( K e. OML /\ K e. CLat /\ K e. AtLat ) )

Proof

Step Hyp Ref Expression
1 hloml 
 |-  ( K e. HL -> K e. OML )
2 hlclat 
 |-  ( K e. HL -> K e. CLat )
3 hlatl 
 |-  ( K e. HL -> K e. AtLat )
4 1 2 3 3jca 
 |-  ( K e. HL -> ( K e. OML /\ K e. CLat /\ K e. AtLat ) )