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 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 A5: 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 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:14;
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 5;

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:50; :: 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 7;
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:66;
then A11: (2 * r) - a <= (a + b) - a by XREAL_1:15;
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
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:8;
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:21;
then r - (min (r - a),r1) >= a by XREAL_1:21;
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, Th10;
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, XBOOLE_1:1; :: 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:50; :: 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 7;
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:66;
then A19: (2 * r) - b >= (a + b) - b by XREAL_1:15;
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
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:21;
then A24: j <= b by A22, XXREAL_0:2;
r - (min (b - r),r1) >= r - (b - r) by A23, XREAL_1:15;
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, Th10;
then N c= Ball x,r1 by PCOMPS_1:1, XXREAL_0:17;
hence N c= X by A9, 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