let r, gg, a, b be Real; 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)); ( 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.]
; ].(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 ;
TARSKI:def 3 ( not i in Ball (x,g) or i in ].(r - g),(r + g).[ )
assume
i in Ball (
x,
g)
;
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;
verum
end;
].(r - g),(r + g).[ c= Ball (x,g)
proof
let i be
object ;
TARSKI:def 3 ( not i in ].(r - g),(r + g).[ or i in Ball (x,g) )
assume A8:
i in ].(r - g),(r + g).[
;
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;
verum
end;
hence
].(r - gg),(r + gg).[ = Ball (x,gg)
by A5; verum