for V being RealUnitarySpace
for u, v, w being Point of V
for r, p being Real st v in (Ball (u,r)) /\ (Ball (w,p)) holds
ex q being Real st
( Ball (v,q) c= Ball (u,r) & Ball (v,q) c= Ball (w,p) )