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 = (|.r1.| + |.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 object st a in (Ball (x1,r1)) \/ (Ball (x2,r2)) holds
a in Ball (x,r)
proof
let a be object ; :: 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 :: thesis: ( ( a in Ball (x1,r1) & a in Ball (x,r) ) or ( a in Ball (x2,r2) & a in Ball (x,r) ) )
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 <= |.r1.| & 0 <= |.r2.| ) by ABSVALUE:4, COMPLEX1:46;
then A3: r1 + 0 <= |.r1.| + |.r2.| by XREAL_1:7;
A4: dist (x,a) < r1 by A2, METRIC_1:11;
0 <= dist (x1,x2) by METRIC_1:5;
then r1 + 0 <= (|.r1.| + |.r2.|) + (dist (x1,x2)) by A3, XREAL_1:7;
then (dist (x,a)) - r < r1 - r1 by A4, XREAL_1:14;
then A5: ((dist (x,a)) - r) + r < 0 + r by XREAL_1:8;
not M is empty by A2;
hence a in Ball (x,r) by A5, METRIC_1:11; :: thesis: verum
end;
case A6: a in Ball (x2,r2) ; :: thesis: a in Ball (x,r)
then dist (x2,a) < r2 by METRIC_1:11;
then (dist (x2,a)) - |.r2.| < r2 - r2 by ABSVALUE:4, XREAL_1:14;
then ( dist (x,a) <= (dist (x1,x2)) + (dist (x2,a)) & ((dist (x2,a)) - |.r2.|) + |.r2.| < 0 + |.r2.| ) by METRIC_1:4, XREAL_1:8;
then (dist (x,a)) - |.r2.| < ((dist (x1,x2)) + (dist (x2,a))) - (dist (x2,a)) by XREAL_1:15;
then ((dist (x,a)) - |.r2.|) - |.r1.| < (dist (x1,x2)) - 0 by COMPLEX1:46, XREAL_1:14;
then A7: ((dist (x,a)) - (|.r1.| + |.r2.|)) + (|.r1.| + |.r2.|) < (|.r1.| + |.r2.|) + (dist (x1,x2)) by XREAL_1:8;
not M is empty by A6;
hence a in Ball (x,r) by A7, METRIC_1:11; :: 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) ; :: thesis: verum