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