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	$$⊢\mathrm{HAtoms}\subseteq {\mathbf{C}}_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		df-at	$$⊢\mathrm{HAtoms}=\left\{x\in {\mathbf{C}}_{\mathscr{H}}|0_{\mathscr{H}}{⋖}_{\mathscr{H}}x\right\}$$
2	1	ssrab3	$$⊢\mathrm{HAtoms}\subseteq {\mathbf{C}}_{\mathscr{H}}$$