let a, b, d, e, r3 be Real; :: thesis:
let PM, PM2 be non empty MetrStruct ; :: thesis:
let x be Element of PM; :: thesis:
let x2 be Element of PM2; :: thesis:
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:
a <= e by A2, A3, XXREAL_0:2;
then A7: a in [.d,e.] by A1, XXREAL_1:1;
let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in Ball (x,r3) ; :: thesis:
then z in { y where y is Element of PM : dist (x,y) < r3 } by METRIC_1:17;
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:10;
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:10, 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 13, TOPMETR:def 1;
real_dist . (x,y) = the distance of PM2 . (x2,y3) by A5, A6, METRIC_1:def 13, 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:17; :: thesis: