theorem :: CARDFIL3:19

for N being RealNormSpace
for x being Element of (MetricSpaceNorm N)
for n being Nat st n <> 0 holds
ex y being Point of N st
( x = y & Ball (x,(1 / n)) = { q where q is Point of N : ||.(y - q).|| < 1 / n } ) by NORMSP_2:2;