let M be MetrSpace; :: thesis: 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
let x1, x2 be Point of M; :: thesis: 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
let r1, r2 be Real; :: thesis: ex x being Point of M ex r being Real st (Ball x1,r1) \/ (Ball x2,r2) c= Ball x,r
reconsider x = x1 as Point of M ;
reconsider r = ((abs r1) + (abs r2)) + (dist x1,x2) as Real ;
take x ; :: thesis: ex r being Real st (Ball x1,r1) \/ (Ball x2,r2) c= Ball x,r
take r ; :: thesis: (Ball x1,r1) \/ (Ball x2,r2) c= Ball x,r
for a being set st a in (Ball x1,r1) \/ (Ball x2,r2) holds
a in Ball x,r

proof

let a be set ; :: thesis: ( a in (Ball x1,r1) \/ (Ball x2,r2) implies a in Ball x,r )
assume A1: a in (Ball x1,r1) \/ (Ball x2,r2) ; :: thesis: a in Ball x,r
then reconsider a = a as Point of M ;

now

per cases ( a in Ball x1,r1 or a in Ball x2,r2 ) by A1, XBOOLE_0:def 3;

case A2: a in Ball x1,r1 ; :: thesis: a in Ball x,r

( r1 <= abs r1 & 0 <= abs r2 ) by ABSVALUE:11, COMPLEX1:132;
then A3: r1 + 0 <= (abs r1) + (abs r2) by XREAL_1:9;
A4: dist x,a < r1 by A2, METRIC_1:12;
0 <= dist x1,x2 by METRIC_1:5;
then r1 + 0 <= ((abs r1) + (abs r2)) + (dist x1,x2) by A3, XREAL_1:9;
then (dist x,a) - r < r1 - r1 by A4, XREAL_1:16;
then A5: ((dist x,a) - r) + r < 0 + r by XREAL_1:10;
not M is empty by A2;
hence a in Ball x,r by A5, METRIC_1:12; :: thesis: verum

end;

case A6: a in Ball x2,r2 ; :: thesis: a in Ball x,r

then dist x2,a < r2 by METRIC_1:12;
then (dist x2,a) - (abs r2) < r2 - r2 by ABSVALUE:11, XREAL_1:16;
then ( dist x,a <= (dist x1,x2) + (dist x2,a) & ((dist x2,a) - (abs r2)) + (abs r2) < 0 + (abs r2) ) by METRIC_1:4, XREAL_1:10;
then (dist x,a) - (abs r2) < ((dist x1,x2) + (dist x2,a)) - (dist x2,a) by XREAL_1:17;
then ((dist x,a) - (abs r2)) - (abs r1) < (dist x1,x2) - 0 by COMPLEX1:132, XREAL_1:16;
then A7: ((dist x,a) - ((abs r1) + (abs r2))) + ((abs r1) + (abs r2)) < ((abs r1) + (abs r2)) + (dist x1,x2) by XREAL_1:10;
not M is empty by A6;
hence a in Ball x,r by A7, METRIC_1:12; :: thesis: verum

end;

end;

end;

hence a in Ball x,r ; :: thesis: verum

end;

hence (Ball x1,r1) \/ (Ball x2,r2) c= Ball x,r by TARSKI:def 3; :: thesis: verum