theorem :: CARDFIL3:17

for N being RealNormSpace
for x being Point of (TopSpaceMetr (MetricSpaceNorm N))
for y being Point of (MetricSpaceNorm N)
for n being positive Nat st x = y holds
Ball (y,(1 / n)) in Balls x