This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 e. CH
	Assertion	hatomici	\|- ( A =/= 0H -> E. x e. HAtoms x C_ A )

Proof

Step	Hyp	Ref	Expression
1		hatomic.1	\|- A e. CH
2	1	chshii	\|- A e. SH
3	2	shatomici	\|- ( A =/= 0H -> E. x e. HAtoms x C_ A )