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:18;
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 14, 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 14, 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 14, TOPMETR:def 1
;
then
real_dist . q1,
x1 < gg
by A7, METRIC_1:10;
then
abs (a9 - r) < gg
by A2, A6, METRIC_1:def 13;
hence
i in ].(r - gg),(r + gg).[
by RCOMP_1:8;
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:14;
abs (a9 - r) < gg
by A8, RCOMP_1:8;
then A9:
real_dist . a9,
r < gg
by METRIC_1:def 13;
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 14, TOPMETR:def 1
;
then
dist x,
a99 < gg
by A2, A9, METRIC_1:10;
hence
i in Ball x,
gg
by METRIC_1:12;
verum
end;
hence
].(r - gg),(r + gg).[ = Ball x,gg
by A5, XBOOLE_0:def 10; verum