let M be 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)
let x1, x2 be 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 r1, r2 be Real; 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
; ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r)
take
r
; (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 ;
( a in (Ball (x1,r1)) \/ (Ball (x2,r2)) implies a in Ball (x,r) )
assume A1:
a in (Ball (x1,r1)) \/ (Ball (x2,r2))
;
a in Ball (x,r)
then reconsider a =
a as
Point of
M ;
now ( ( 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)
;
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;
verum end; case A6:
a in Ball (
x2,
r2)
;
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;
verum end; end; end;
hence
a in Ball (
x,
r)
;
verum
end;
hence
(Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r)
; verum