Theorem hatomici

Description: The Hilbert lattice is atomic, i.e. any nonzero element is greater than or equal to some atom. Remark in Kalmbach p. 140. (Contributed by NM, 22-Jul-2001) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hatomic.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	hatomici	$$⊢A\ne 0_{\mathscr{H}}\to \exists x\in \mathrm{HAtoms}x\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		hatomic.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	chshii	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
3	2	shatomici	$$⊢A\ne 0_{\mathscr{H}}\to \exists x\in \mathrm{HAtoms}x\subseteq A$$