let a, b be Real; :: thesis: for X being Subset of REAL st a < b & not a in X & not b in X & X in Family_open_set (Closed-Interval-MSpace (a,b)) holds
X is open
let X be Subset of REAL; :: thesis: ( a < b & not a in X & not b in X & X in Family_open_set (Closed-Interval-MSpace (a,b)) implies X is open )
assume that
A1: a < b and
A2: not a in X and
A3: not b in X ; :: thesis: ( not X in Family_open_set (Closed-Interval-MSpace (a,b)) or X is open )
assume A4: X in Family_open_set (Closed-Interval-MSpace (a,b)) ; :: thesis: X is open
then reconsider V = X as Subset of (Closed-Interval-MSpace (a,b)) ;
for r being Element of REAL st r in X holds
ex N being Neighbourhood of r st N c= X

proof

let r be Element of REAL ; :: thesis: ( r in X implies ex N being Neighbourhood of r st N c= X )
assume A5: r in X ; :: thesis: ex N being Neighbourhood of r st N c= X
reconsider r = r as Real ;
r in V by A5;
then reconsider x = r as Element of (Closed-Interval-MSpace (a,b)) ;
the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by A1, TOPMETR:10;
then x in [.a,b.] ;
then x in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def 1;
then A6: ex r2 being Real st
( r2 = x & a <= r2 & r2 <= b ) ;
A7: r - a <> 0 by A2, A5;
ex N being Neighbourhood of r st N c= X

proof

consider r1 being Real such that
A8: r1 > 0 and
A9: Ball (x,r1) c= X by A4, A5, PCOMPS_1:def 4;

per cases ( r <= (a + b) / 2 or r > (a + b) / 2 ) ;

suppose A10: r <= (a + b) / 2 ; :: thesis: ex N being Neighbourhood of r st N c= X

set gg = min ((r - a),r1);
min ((r - a),r1) > 0

proof

per cases ( min ((r - a),r1) = r - a or min ((r - a),r1) = r1 ) by XXREAL_0:15;

suppose min ((r - a),r1) = r - a ; :: thesis: min ((r - a),r1) > 0

hence min ((r - a),r1) > 0 by A7, A6, XREAL_1:48; :: thesis: verum

end;

suppose min ((r - a),r1) = r1 ; :: thesis: min ((r - a),r1) > 0

hence min ((r - a),r1) > 0 by A8; :: thesis: verum

end;

end;

end;

then reconsider N = ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ as Neighbourhood of r by RCOMP_1:def 6;
take N ; :: thesis: N c= X
].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ c= [.a,b.]

proof

2 * r <= 2 * ((a + b) / 2) by A10, XREAL_1:64;
then A11: (2 * r) - a <= (a + b) - a by XREAL_1:13;
let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ or i in [.a,b.] )
assume i in ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ ; :: thesis: i in [.a,b.]
then i in { l where l is Real : ( r - (min ((r - a),r1)) < l & l < r + (min ((r - a),r1)) ) } by RCOMP_1:def 2;
then consider j being Real such that
A12: j = i and
A13: r - (min ((r - a),r1)) < j and
A14: j < r + (min ((r - a),r1)) ;
A15: min ((r - a),r1) <= r - a by XXREAL_0:17;
then r + (min ((r - a),r1)) <= r + (r - a) by XREAL_1:6;
then r + (min ((r - a),r1)) <= (a + b) - a by A11, XXREAL_0:2;
then A16: j <= b by A14, XXREAL_0:2;
(min ((r - a),r1)) + a <= r by A15, XREAL_1:19;
then r - (min ((r - a),r1)) >= a by XREAL_1:19;
then a <= j by A13, XXREAL_0:2;
then j in { l where l is Real : ( a <= l & l <= b ) } by A16;
hence i in [.a,b.] by A12, RCOMP_1:def 1; :: thesis: verum

end;

then ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ = Ball (x,(min ((r - a),r1))) by A1, Th9;
then ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ c= Ball (x,r1) by PCOMPS_1:1, XXREAL_0:17;
hence N c= X by A9; :: thesis: verum

end;

suppose A17: r > (a + b) / 2 ; :: thesis: ex N being Neighbourhood of r st N c= X

set gg = min ((b - r),r1);
A18: b - r <> 0 by A3, A5;
min ((b - r),r1) > 0

proof

per cases ( min ((b - r),r1) = b - r or min ((b - r),r1) = r1 ) by XXREAL_0:15;

suppose min ((b - r),r1) = b - r ; :: thesis: min ((b - r),r1) > 0

hence min ((b - r),r1) > 0 by A6, A18, XREAL_1:48; :: thesis: verum

end;

suppose min ((b - r),r1) = r1 ; :: thesis: min ((b - r),r1) > 0

hence min ((b - r),r1) > 0 by A8; :: thesis: verum

end;

end;

end;

then reconsider N = ].(r - (min ((b - r),r1))),(r + (min ((b - r),r1))).[ as Neighbourhood of r by RCOMP_1:def 6;
take N ; :: thesis: N c= X
].(r - (min ((b - r),r1))),(r + (min ((b - r),r1))).[ c= [.a,b.]

proof

2 * r >= ((a + b) / 2) * 2 by A17, XREAL_1:64;
then A19: (2 * r) - b >= (a + b) - b by XREAL_1:13;
let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in ].(r - (min ((b - r),r1))),(r + (min ((b - r),r1))).[ or i in [.a,b.] )
assume i in ].(r - (min ((b - r),r1))),(r + (min ((b - r),r1))).[ ; :: thesis: i in [.a,b.]
then i in { l where l is Real : ( r - (min ((b - r),r1)) < l & l < r + (min ((b - r),r1)) ) } by RCOMP_1:def 2;
then consider j being Real such that
A20: j = i and
A21: r - (min ((b - r),r1)) < j and
A22: j < r + (min ((b - r),r1)) ;
A23: min ((b - r),r1) <= b - r by XXREAL_0:17;
then r + (min ((b - r),r1)) <= b by XREAL_1:19;
then A24: j <= b by A22, XXREAL_0:2;
r - (min ((b - r),r1)) >= r - (b - r) by A23, XREAL_1:13;
then r - (min ((b - r),r1)) >= a by A19, XXREAL_0:2;
then a <= j by A21, XXREAL_0:2;
then j in { l where l is Real : ( a <= l & l <= b ) } by A24;
hence i in [.a,b.] by A20, RCOMP_1:def 1; :: thesis: verum

end;

then ].(r - (min ((b - r),r1))),(r + (min ((b - r),r1))).[ = Ball (x,(min ((b - r),r1))) by A1, Th9;
then N c= Ball (x,r1) by PCOMPS_1:1, XXREAL_0:17;
hence N c= X by A9; :: thesis: verum

end;

end;

end;

hence ex N being Neighbourhood of r st N c= X ; :: thesis: verum

end;

hence X is open by RCOMP_1:20; :: thesis: verum