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 ) |
| 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 ) |