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 A1: ( a < b & not a in X & not b in X ) ; :: thesis: ( not X in Family_open_set (Closed-Interval-MSpace a,b) or X is open )
assume A2: 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 real number st r in X holds
ex N being Neighbourhood of r st N c= X

proof

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

proof

consider r1 being Real such that
A6: ( r1 > 0 & Ball x,r1 c= X ) by A2, A3, PCOMPS_1:def 5;

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

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

set gg = min (r - a),r1;
A8: 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 A4, A5, XREAL_1:50; :: thesis: verum

end;

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

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

end;

end;

end;

A9: ].(r - (min (r - a),r1)),(r + (min (r - a),r1)).[ c= Ball x,r1

proof

].(r - (min (r - a),r1)),(r + (min (r - a),r1)).[ c= [.a,b.]

proof

let i be set ; :: 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
A10: ( j = i & r - (min (r - a),r1) < j & j < r + (min (r - a),r1) ) ;
2 * r <= 2 * ((a + b) / 2) by A7, XREAL_1:66;
then A11: (2 * r) - a <= (a + b) - a by XREAL_1:15;
A12: min (r - a),r1 <= r - a by XXREAL_0:17;
then r + (min (r - a),r1) <= r + (r - a) by XREAL_1:8;
then A13: r + (min (r - a),r1) <= (a + b) - a by A11, XXREAL_0:2;
(min (r - a),r1) + a <= r by A12, XREAL_1:21;
then r - (min (r - a),r1) >= a by XREAL_1:21;
then A14: a <= j by A10, XXREAL_0:2;
j <= b by A10, A13, XXREAL_0:2;
then j in { l where l is Real : ( a <= l & l <= b ) } by A14;
hence i in [.a,b.] by A10, 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, A8, Th10;
hence ].(r - (min (r - a),r1)),(r + (min (r - a),r1)).[ c= Ball x,r1 by PCOMPS_1:1, XXREAL_0:17; :: thesis: verum

end;

reconsider N = ].(r - (min (r - a),r1)),(r + (min (r - a),r1)).[ as Neighbourhood of r by A8, RCOMP_1:def 7;
take N ; :: thesis: N c= X
thus N c= X by A6, A9, XBOOLE_1:1; :: thesis: verum

end;

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

set gg = min (b - r),r1;
A16: b - r <> 0 by A1, A3;
A17: 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 A5, A16, XREAL_1:50; :: thesis: verum

end;

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

hence min (b - r),r1 > 0 by A6; :: 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 7;
take N ; :: thesis: N c= X
N c= Ball x,r1

proof

].(r - (min (b - r),r1)),(r + (min (b - r),r1)).[ c= [.a,b.]

proof

let i be set ; :: 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
A18: ( j = i & r - (min (b - r),r1) < j & j < r + (min (b - r),r1) ) ;
A19: min (b - r),r1 <= b - r by XXREAL_0:17;
2 * r >= ((a + b) / 2) * 2 by A15, XREAL_1:66;
then A20: (2 * r) - b >= (a + b) - b by XREAL_1:15;
r - (min (b - r),r1) >= r - (b - r) by A19, XREAL_1:15;
then r - (min (b - r),r1) >= a by A20, XXREAL_0:2;
then A21: a <= j by A18, XXREAL_0:2;
r + (min (b - r),r1) <= b by A19, XREAL_1:21;
then j <= b by A18, XXREAL_0:2;
then j in { l where l is Real : ( a <= l & l <= b ) } by A21;
hence i in [.a,b.] by A18, 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, A17, Th10;
hence N c= Ball x,r1 by PCOMPS_1:1, XXREAL_0:17; :: thesis: verum

end;

hence N c= X by A6, XBOOLE_1:1; :: 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:41; :: thesis: verum