let r, gg, a, b be Real; :: thesis: for x being Element of (Closed-Interval-MSpace a,b) st a <= b & x = r & gg > 0 & ].(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 & gg > 0 & ].(r - gg),(r + gg).[ c= [.a,b.] implies ].(r - gg),(r + gg).[ = Ball x,gg )
assume A1: ( a <= b & x = r & gg > 0 & ].(r - gg),(r + gg).[ c= [.a,b.] ) ; :: thesis: ].(r - gg),(r + gg).[ = Ball x,gg
set g = gg;
set CM = Closed-Interval-MSpace a,b;
A2: the carrier of (Closed-Interval-MSpace a,b) c= the carrier of RealSpace by TOPMETR:def 1;
set N1 = Ball x,gg;
Ball x,gg = ].(r - gg),(r + gg).[

proof

thus Ball x,gg c= ].(r - gg),(r + gg).[ :: according to XBOOLE_0:def 10 :: thesis: ].(r - gg),(r + gg).[ c= Ball x,gg

proof

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in Ball x,gg or i in ].(r - gg),(r + gg).[ )
assume i in Ball x,gg ; :: thesis: i in ].(r - gg),(r + gg).[
then i in { q where q is Element of (Closed-Interval-MSpace a,b) : dist x,q < gg } by METRIC_1:18;
then consider q being Element of (Closed-Interval-MSpace a,b) such that
A3: ( q = i & dist x,q < gg ) ;
reconsider a' = i as Real by A2, A3, METRIC_1:def 14, TARSKI:def 3;
reconsider x1 = x, q1 = q as Element of REAL by A2, METRIC_1:def 14, TARSKI:def 3;
reconsider x2 = x, q2 = q as Element of (Closed-Interval-MSpace a,b) ;
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 14, TOPMETR:def 1 ;
then real_dist . q1,x1 < gg by A3, METRIC_1:10;
then abs (a' - r) < gg by A1, A3, METRIC_1:def 13;
hence i in ].(r - gg),(r + gg).[ by RCOMP_1:8; :: thesis: verum

end;

thus ].(r - gg),(r + gg).[ c= Ball x,gg :: thesis: verum

proof

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in ].(r - gg),(r + gg).[ or i in Ball x,gg )
assume A4: i in ].(r - gg),(r + gg).[ ; :: thesis: i in Ball x,gg
then reconsider a' = i as Real ;
reconsider a'' = i as Element of (Closed-Interval-MSpace a,b) by A1, A4, TOPMETR:14;
A5: dist x,a'' = the distance of (Closed-Interval-MSpace a,b) . x,a'' by METRIC_1:def 1
.= real_dist . x,a'' by METRIC_1:def 14, TOPMETR:def 1 ;
abs (a' - r) < gg by A4, RCOMP_1:8;
then real_dist . a',r < gg by METRIC_1:def 13;
then dist x,a'' < gg by A1, A5, METRIC_1:10;
hence i in Ball x,gg by METRIC_1:12; :: thesis: verum

end;

end;

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