Metamath Proof Explorer

Theorem atelch

Description: An atom is a Hilbert lattice element. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atelch 
|- ( A e. HAtoms -> A e. CH )

Proof

Step Hyp Ref Expression
1 atssch 
 |-  HAtoms C_ CH
2 1 sseli 
 |-  ( A e. HAtoms -> A e. CH )