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ℋ