for M being MetrSpace
for x1, x2 being Point of M
for r1, r2 being Real ex x being Point of M ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r)