let X be open Subset of REAL ; :: thesis: for a, b being Real st X c= [.a,b.] holds
( not a in X & not b in X )
let a, b be Real; :: thesis: ( X c= [.a,b.] implies ( not a in X & not b in X ) )
assume A1: X c= [.a,b.] ; :: thesis: ( not a in X & not b in X )
assume A2: ( a in X or b in X ) ; :: thesis: contradiction

per cases ( a in X or b in X ) by A2;

suppose a in X ; :: thesis: contradiction

then consider g being real number such that
A3: ( 0 < g & ].(a - g),(a + g).[ c= X ) by RCOMP_1:40;
A4: g / 2 <> 0 by A3;
A5: a - (g / 2) < a - 0 by A3, A4, XREAL_1:17;
A6: a + 0 < a + g by A3, XREAL_1:10;
A7: ].(a - g),(a + g).[ c= [.a,b.] by A1, A3, XBOOLE_1:1;
g > g / 2 by A3, XREAL_1:218;
then ( a - g < a - (g / 2) & a - (g / 2) < a + g ) by A5, A6, XREAL_1:17, XXREAL_0:2;
then a - (g / 2) in { l where l is Real : ( a - g < l & l < a + g ) } ;
then a - (g / 2) in ].(a - g),(a + g).[ by RCOMP_1:def 2;
then a - (g / 2) in [.a,b.] by A7;
then a - (g / 2) in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def 1;
then consider l being Real such that
A8: ( l = a - (g / 2) & a <= l & l <= b ) ;
thus contradiction by A5, A8; :: thesis: verum

end;

suppose b in X ; :: thesis: contradiction

then consider g being real number such that
A9: ( 0 < g & ].(b - g),(b + g).[ c= X ) by RCOMP_1:40;
A10: g / 2 <> 0 by A9;
A11: b + (g / 2) > b + 0 by A9, A10, XREAL_1:8;
A12: ].(b - g),(b + g).[ c= [.a,b.] by A1, A9, XBOOLE_1:1;
A13: g > g / 2 by A9, XREAL_1:218;
A14: b - g < b - 0 by A9, XREAL_1:17;
A15: b + (g / 2) < b + g by A13, XREAL_1:10;
b - g < b + (g / 2) by A11, A14, XXREAL_0:2;
then b + (g / 2) in { l where l is Real : ( b - g < l & l < b + g ) } by A15;
then b + (g / 2) in ].(b - g),(b + g).[ by RCOMP_1:def 2;
then b + (g / 2) in [.a,b.] by A12;
then b + (g / 2) in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def 1;
then consider l being Real such that
A16: ( l = b + (g / 2) & a <= l & l <= b ) ;
thus contradiction by A11, A16; :: thesis: verum

end;

end;