let a, b be Real; for X being Subset of REAL
for V being Subset of (Closed-Interval-MSpace (a,b)) st V = X & X is open holds
V in Family_open_set (Closed-Interval-MSpace (a,b))
let X be Subset of REAL; for V being Subset of (Closed-Interval-MSpace (a,b)) st V = X & X is open holds
V in Family_open_set (Closed-Interval-MSpace (a,b))
let V be Subset of (Closed-Interval-MSpace (a,b)); ( V = X & X is open implies V in Family_open_set (Closed-Interval-MSpace (a,b)) )
assume A1:
V = X
; ( not X is open or V in Family_open_set (Closed-Interval-MSpace (a,b)) )
assume A2:
X is open
; V in Family_open_set (Closed-Interval-MSpace (a,b))
for x being Element of (Closed-Interval-MSpace (a,b)) st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V )
proof
let x be
Element of
(Closed-Interval-MSpace (a,b));
( x in V implies ex r being Real st
( r > 0 & Ball (x,r) c= V ) )
assume A3:
x in V
;
ex r being Real st
( r > 0 & Ball (x,r) c= V )
then reconsider r =
x as
Element of
REAL by A1;
consider N being
Neighbourhood of
r such that A4:
N c= X
by A1, A2, A3, RCOMP_1:18;
consider g being
Real such that A5:
0 < g
and A6:
N = ].(r - g),(r + g).[
by RCOMP_1:def 6;
reconsider g =
g as
Element of
REAL by XREAL_0:def 1;
A7:
Ball (
x,
g)
c= N
proof
let aa be
object ;
TARSKI:def 3 ( not aa in Ball (x,g) or aa in N )
assume
aa in Ball (
x,
g)
;
aa in N
then
aa 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 A8:
q = aa
and A9:
dist (
x,
q)
< g
;
A10:
(
q in the
carrier of
(Closed-Interval-MSpace (a,b)) & the
carrier of
(Closed-Interval-MSpace (a,b)) c= the
carrier of
RealSpace )
by TOPMETR:def 1;
then reconsider a9 =
aa as
Real by A8;
reconsider x1 =
x,
q1 =
q as
Element of
REAL by A10, METRIC_1:def 13;
dist (
x,
q) =
the
distance of
(Closed-Interval-MSpace (a,b)) . (
x,
q)
by METRIC_1:def 1
.=
real_dist . (
x,
q)
by METRIC_1:def 13, TOPMETR:def 1
;
then
real_dist . (
q1,
x1)
< g
by A9, METRIC_1:9;
then
|.(a9 - r).| < g
by A8, METRIC_1:def 12;
hence
aa in N
by A6, RCOMP_1:1;
verum
end;
N c= Ball (
x,
g)
proof
let aa be
object ;
TARSKI:def 3 ( not aa in N or aa in Ball (x,g) )
assume A11:
aa in N
;
aa in Ball (x,g)
then reconsider a9 =
aa as
Element of
REAL ;
|.(a9 - r).| < g
by A6, A11, RCOMP_1:1;
then A12:
real_dist . (
a9,
r)
< g
by METRIC_1:def 12;
aa in X
by A4, A11;
then reconsider a99 =
aa,
r9 =
r as
Element of
(Closed-Interval-MSpace (a,b)) by A1;
dist (
r9,
a99) =
the
distance of
(Closed-Interval-MSpace (a,b)) . (
r9,
a99)
by METRIC_1:def 1
.=
real_dist . (
r9,
a99)
by METRIC_1:def 13, TOPMETR:def 1
;
then
dist (
r9,
a99)
< g
by A12, METRIC_1:9;
hence
aa in Ball (
x,
g)
by METRIC_1:11;
verum
end;
then
N = Ball (
x,
g)
by A7;
hence
ex
r being
Real st
(
r > 0 &
Ball (
x,
r)
c= V )
by A1, A4, A5;
verum
end;
hence
V in Family_open_set (Closed-Interval-MSpace (a,b))
by PCOMPS_1:def 4; verum