Metamath Proof Explorer


Theorem atssch

Description: Atoms are a subset of the Hilbert lattice. (Contributed by NM, 14-Aug-2002) (New usage is discouraged.)

Ref Expression
Assertion atssch HAtoms ⊆ C

Proof

Step Hyp Ref Expression
1 df-at HAtoms = { 𝑥C ∣ 0 𝑥 }
2 1 ssrab3 HAtoms ⊆ C