for V being RealUnitarySpace
for v, u being Point of V
for r being Real st u in Ball (v,r) holds
ex p being Real st
( p > 0 & Ball (u,p) c= Ball (v,r) )