for X being RealUnitarySpace
for x, z being Point of X
for r being Real holds
( z in Ball (x,r) iff ||.(x - z).|| < r )