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)
set g = gg;
set CM = Closed-Interval-MSpace (a,b);
set N1 = Ball (x,gg);
A4:
the carrier of (Closed-Interval-MSpace (a,b)) c= the carrier of RealSpace
by TOPMETR:def 1;
A5:
Ball (x,gg) c= ].(r - gg),(r + gg).[
proof
let i be
set ;
TARSKI:def 3 ( not i in Ball (x,gg) or i in ].(r - gg),(r + gg).[ )
assume
i in Ball (
x,
gg)
;
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:17;
then consider q being
Element of
(Closed-Interval-MSpace (a,b)) such that A6:
q = i
and A7:
dist (
x,
q)
< gg
;
reconsider a9 =
i as
Real by A4, A6, METRIC_1:def 13, TARSKI:def 3;
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, TARSKI:def 3;
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)
< gg
by A7, METRIC_1:9;
then
abs (a9 - r) < gg
by A2, A6, METRIC_1:def 12;
hence
i in ].(r - gg),(r + gg).[
by RCOMP_1:1;
verum
end;
].(r - gg),(r + gg).[ c= Ball (x,gg)
proof
let i be
set ;
TARSKI:def 3 ( not i in ].(r - gg),(r + gg).[ or i in Ball (x,gg) )
assume A8:
i in ].(r - gg),(r + gg).[
;
i in Ball (x,gg)
then reconsider a9 =
i as
Real ;
reconsider a99 =
i as
Element of
(Closed-Interval-MSpace (a,b)) by A1, A3, A8, TOPMETR:10;
abs (a9 - r) < gg
by A8, RCOMP_1:1;
then A9:
real_dist . (
a9,
r)
< gg
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)
< gg
by A2, A9, METRIC_1:9;
hence
i in Ball (
x,
gg)
by METRIC_1:11;
verum
end;
hence
].(r - gg),(r + gg).[ = Ball (x,gg)
by A5, XBOOLE_0:def 10; verum