let a, b be Real; :: thesis: 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; :: thesis: 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)); :: thesis: ( V = X & X is open implies V in Family_open_set (Closed-Interval-MSpace (a,b)) )
assume A1: V = X ; :: thesis: ( not X is open or V in Family_open_set (Closed-Interval-MSpace (a,b)) )
assume A2: X is open ; :: thesis: 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)); :: thesis: ( x in V implies ex r being Real st
( r > 0 & Ball (x,r) c= V ) )
assume A3: x in V ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not aa in Ball (x,g) or aa in N )
assume aa in Ball (x,g) ; :: thesis: 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; :: thesis: verum

end;

N c= Ball (x,g)

proof

let aa be object ; :: according to TARSKI:def 3 :: thesis: ( not aa in N or aa in Ball (x,g) )
assume A11: aa in N ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

hence V in Family_open_set (Closed-Interval-MSpace (a,b)) by PCOMPS_1:def 4; :: thesis: verum