theorem :: CARDFIL3:18

for N being RealNormSpace
for x being Point of (MetricSpaceNorm N)
for n being Nat st n <> 0 holds
Ball (x,(1 / n)) = { q where q is Element of (MetricSpaceNorm N) : dist (x,q) < 1 / n } by METRIC_1:def 14;