for X being RealUnitarySpace
for x, z being Point of X
for r being Real holds
( z in cl_Ball (x,r) iff dist (x,z) <= r )