theorem :: CARDFIL3:16

for N being RealNormSpace
for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) ex y being Point of (MetricSpaceNorm N) st
( y = x & Balls x = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } ) by FRECHET:def 1;