for V being RealUnitarySpace
for v being Point of V ex r being Real st
( r > 0 & Ball (v,r) c= the carrier of V )