let r, gg, a, b be Real; :: thesis: for x being Element of (Closed-Interval-MSpace (a,b)) st a <= b & x = r & ].(r - gg),(r + gg).[ c= [.a,b.] holds
].(r - gg),(r + gg).[ = Ball (x,gg)
let x be Element of (Closed-Interval-MSpace (a,b)); :: thesis: ( a <= b & x = r & ].(r - gg),(r + gg).[ c= [.a,b.] implies ].(r - gg),(r + gg).[ = Ball (x,gg) )
assume that
A1: a <= b and
A2: x = r and
A3: ].(r - gg),(r + gg).[ c= [.a,b.] ; :: thesis: ].(r - gg),(r + gg).[ = Ball (x,gg)
reconsider g = gg as Element of REAL by XREAL_0:def 1;
reconsider r = r as Element of REAL by XREAL_0:def 1;
set CM = Closed-Interval-MSpace (a,b);
set N1 = Ball (x,g);
A4: the carrier of (Closed-Interval-MSpace (a,b)) c= the carrier of RealSpace by TOPMETR:def 1;
A5: Ball (x,g) c= ].(r - g),(r + g).[

proof

let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in Ball (x,g) or i in ].(r - g),(r + g).[ )
assume i in Ball (x,g) ; :: thesis: i in ].(r - g),(r + g).[
then i in { q where q is Element of (Closed-Interval-MSpace (a,b)) : dist (x,q) < g } by METRIC_1:17;
then consider q being Element of (Closed-Interval-MSpace (a,b)) such that
A6: q = i and
A7: dist (x,q) < g ;
reconsider a9 = i as Element of REAL by A4, A6, METRIC_1:def 13;
reconsider x2 = x, q2 = q as Element of (Closed-Interval-MSpace (a,b)) ;
reconsider x1 = x, q1 = q as Element of REAL by A4, METRIC_1:def 13;
dist (x2,q2) = the distance of (Closed-Interval-MSpace (a,b)) . (x2,q2) by METRIC_1:def 1
.= real_dist . (x2,q2) by METRIC_1:def 13, TOPMETR:def 1 ;
then real_dist . (q1,x1) < g by A7, METRIC_1:9;
then |.(a9 - r).| < g by A2, A6, METRIC_1:def 12;
hence i in ].(r - g),(r + g).[ by RCOMP_1:1; :: thesis: verum

end;

].(r - g),(r + g).[ c= Ball (x,g)

proof

let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in ].(r - g),(r + g).[ or i in Ball (x,g) )
assume A8: i in ].(r - g),(r + g).[ ; :: thesis: i in Ball (x,g)
then reconsider a9 = i as Element of REAL ;
reconsider a99 = i as Element of (Closed-Interval-MSpace (a,b)) by A1, A3, A8, TOPMETR:10;
|.(a9 - r).| < g by A8, RCOMP_1:1;
then A9: real_dist . (a9,r) < g by METRIC_1:def 12;
dist (x,a99) = the distance of (Closed-Interval-MSpace (a,b)) . (x,a99) by METRIC_1:def 1
.= real_dist . (x,a99) by METRIC_1:def 13, TOPMETR:def 1 ;
then dist (x,a99) < g by A2, A9, METRIC_1:9;
hence i in Ball (x,g) by METRIC_1:11; :: thesis: verum

end;

hence ].(r - gg),(r + gg).[ = Ball (x,gg) by A5; :: thesis: verum