theorem Th41: :: BHSP_2:41
for X being RealUnitarySpace
for x, z being Point of X
for r being Real holds
( z in Ball (x,r) iff dist (x,z) < r )