let V be RealUnitarySpace; :: thesis: for v1, v2 being Point of V
for r1, r2 being Real ex u being Point of V ex r being Real st (Ball (v1,r1)) \/ (Ball (v2,r2)) c= Ball (u,r)
let v1, v2 be Point of V; :: thesis: for r1, r2 being Real ex u being Point of V ex r being Real st (Ball (v1,r1)) \/ (Ball (v2,r2)) c= Ball (u,r)
let r1, r2 be Real; :: thesis: ex u being Point of V ex r being Real st (Ball (v1,r1)) \/ (Ball (v2,r2)) c= Ball (u,r)
reconsider u = v1 as Point of V ;
reconsider r = ((abs r1) + (abs r2)) + (dist (v1,v2)) as Real ;
take u ; :: thesis: ex r being Real st (Ball (v1,r1)) \/ (Ball (v2,r2)) c= Ball (u,r)
take r ; :: thesis: (Ball (v1,r1)) \/ (Ball (v2,r2)) c= Ball (u,r)
for a being set st a in (Ball (v1,r1)) \/ (Ball (v2,r2)) holds
a in Ball (u,r)

proof

let a be set ; :: thesis: ( a in (Ball (v1,r1)) \/ (Ball (v2,r2)) implies a in Ball (u,r) )
assume A1: a in (Ball (v1,r1)) \/ (Ball (v2,r2)) ; :: thesis: a in Ball (u,r)
then reconsider a = a as Point of V ;

now

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

case a in Ball (v1,r1) ; :: thesis: a in Ball (u,r)

then A2: dist (u,a) < r1 by BHSP_2:41;
( r1 <= abs r1 & 0 <= abs r2 ) by ABSVALUE:4, COMPLEX1:46;
then A3: r1 + 0 <= (abs r1) + (abs r2) by XREAL_1:7;
0 <= dist (v1,v2) by BHSP_1:37;
then r1 + 0 <= ((abs r1) + (abs r2)) + (dist (v1,v2)) by A3, XREAL_1:7;
then (dist (u,a)) - r < r1 - r1 by A2, XREAL_1:14;
then ((dist (u,a)) - r) + r < 0 + r by XREAL_1:8;
hence a in Ball (u,r) by BHSP_2:41; :: thesis: verum

end;

case a in Ball (v2,r2) ; :: thesis: a in Ball (u,r)

then dist (v2,a) < r2 by BHSP_2:41;
then (dist (v2,a)) - (abs r2) < r2 - r2 by ABSVALUE:4, XREAL_1:14;
then ((dist (v2,a)) - (abs r2)) + (abs r2) < 0 + (abs r2) by XREAL_1:8;
then (dist (u,a)) - (abs r2) < ((dist (v1,v2)) + (dist (v2,a))) - (dist (v2,a)) by BHSP_1:35, XREAL_1:15;
then ((dist (u,a)) - (abs r2)) - (abs r1) < (dist (v1,v2)) - 0 by COMPLEX1:46, XREAL_1:14;
then ((dist (u,a)) - ((abs r1) + (abs r2))) + ((abs r1) + (abs r2)) < ((abs r1) + (abs r2)) + (dist (v1,v2)) by XREAL_1:8;
hence a in Ball (u,r) by BHSP_2:41; :: thesis: verum

end;

end;

end;

hence a in Ball (u,r) ; :: thesis: verum

end;

hence (Ball (v1,r1)) \/ (Ball (v2,r2)) c= Ball (u,r) by TARSKI:def 3; :: thesis: verum