Metamath Proof Explorer


Theorem ela

Description: Atoms in a Hilbert lattice are the elements that cover the zero subspace. Definition of atom in Kalmbach p. 15. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion ela AHAtomsAC0A

Proof

Step Hyp Ref Expression
1 breq2 x=A0x0A
2 df-at HAtoms=xC|0x
3 1 2 elrab2 AHAtomsAC0A