theorem :: BHSP_2:45

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