theorem Th3: :: NORMSP_2:3

for X being RealNormSpace
for z being Element of (MetricSpaceNorm X)
for r being Real ex x being Point of X st
( x = z & cl_Ball (z,r) = { y where y is Point of X : ||.(x - y).|| <= r } )