for X being RealUnitarySpace
for x, y, z being Point of X
for r being Real st y in Ball (x,r) holds
y - z in Ball ((x - z),r)