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	⊢ 𝐴 ∈ Cℋ
Assertion	hatomici	⊢ ( 𝐴 ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		hatomic.1	⊢ 𝐴 ∈ Cℋ
2	1	chshii	⊢ 𝐴 ∈ Sℋ
3	2	shatomici	⊢ ( 𝐴 ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 )