let a, b, d, e, r3 be Real; :: thesis: for PM, PM2 being non empty MetrStruct
for x being Element of PM
for x2 being Element of PM2 st d <= a & a <= b & b <= e & PM = Closed-Interval-MSpace a,b & PM2 = Closed-Interval-MSpace d,e & x = x2 holds
Ball x,r3 c= Ball x2,r3
let PM, PM2 be non empty MetrStruct ; :: thesis: for x being Element of PM
for x2 being Element of PM2 st d <= a & a <= b & b <= e & PM = Closed-Interval-MSpace a,b & PM2 = Closed-Interval-MSpace d,e & x = x2 holds
Ball x,r3 c= Ball x2,r3
let x be Element of PM; :: thesis: for x2 being Element of PM2 st d <= a & a <= b & b <= e & PM = Closed-Interval-MSpace a,b & PM2 = Closed-Interval-MSpace d,e & x = x2 holds
Ball x,r3 c= Ball x2,r3
let x2 be Element of PM2; :: thesis: ( d <= a & a <= b & b <= e & PM = Closed-Interval-MSpace a,b & PM2 = Closed-Interval-MSpace d,e & x = x2 implies Ball x,r3 c= Ball x2,r3 )
assume that
A1: d <= a and
A2: a <= b and
A3: b <= e and
A4: PM = Closed-Interval-MSpace a,b and
A5: PM2 = Closed-Interval-MSpace d,e and
A6: x = x2 ; :: thesis: Ball x,r3 c= Ball x2,r3
a <= e by A2, A3, XXREAL_0:2;
then A7: a in [.d,e.] by A1, XXREAL_1:1;
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Ball x,r3 or z in Ball x2,r3 )
assume z in Ball x,r3 ; :: thesis: z in Ball x2,r3
then z in { y where y is Element of PM : dist x,y < r3 } by METRIC_1:18;
then consider y being Element of PM such that
A8: ( y = z & dist x,y < r3 ) ;
the carrier of PM = [.a,b.] by A2, A4, TOPMETR:14;
then A9: y in [.a,b.] ;
A10: d <= b by A1, A2, XXREAL_0:2;
then b in [.d,e.] by A3, XXREAL_1:1;
then [.a,b.] c= [.d,e.] by A7, XXREAL_2:def 12;
then reconsider y3 = y as Element of PM2 by A3, A5, A10, A9, TOPMETR:14, XXREAL_0:2;
A11: dist x,y = the distance of PM . x,y by METRIC_1:def 1;
A12: the distance of PM . x,y = real_dist . x,y by A4, METRIC_1:def 14, TOPMETR:def 1;
real_dist . x,y = the distance of PM2 . x2,y3 by A5, A6, METRIC_1:def 14, TOPMETR:def 1
.= dist x2,y3 by METRIC_1:def 1 ;
then z in { y2 where y2 is Element of PM2 : dist x2,y2 < r3 } by A8, A12, A11;
hence z in Ball x2,r3 by METRIC_1:18; :: thesis: verum