theorem Th13: :: RUSUB_7:13
for S being RealUnitarySpace
for x being Point of S
for y being Point of (MetricSpaceNorm (RUSp2RNSp S))
for r being Real st x = y holds
Ball (x,r) = Ball (y,r)