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 such that
A3: 0 < g and
A4: ].(a - g),(a + g).[ c= X by RCOMP_1:19;
g / 2 <> 0 by A3;
then A5: a - (g / 2) < a - 0 by A3, XREAL_1:15;
g > g / 2 by A3, XREAL_1:216;
then A6: a - g < a - (g / 2) by XREAL_1:15;
a + 0 < a + g by A3, XREAL_1:8;
then a - (g / 2) < a + g by A5, XXREAL_0:2;
then a - (g / 2) in { l where l is Real : ( a - g < l & l < a + g ) } by A6;
then A7: a - (g / 2) in ].(a - g),(a + g).[ by RCOMP_1:def 2;
].(a - g),(a + g).[ c= [.a,b.] by A1, A4;
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 ex l being Real st
( l = a - (g / 2) & a <= l & l <= b ) ;
hence contradiction by A5; :: thesis: verum

end;

suppose b in X ; :: thesis: contradiction

then consider g being Real such that
A8: 0 < g and
A9: ].(b - g),(b + g).[ c= X by RCOMP_1:19;
g / 2 <> 0 by A8;
then A10: b + (g / 2) > b + 0 by A8, XREAL_1:6;
g > g / 2 by A8, XREAL_1:216;
then A11: b + (g / 2) < b + g by XREAL_1:8;
b - g < b - 0 by A8, XREAL_1:15;
then b - g < b + (g / 2) by A10, XXREAL_0:2;
then b + (g / 2) in { l where l is Real : ( b - g < l & l < b + g ) } by A11;
then A12: b + (g / 2) in ].(b - g),(b + g).[ by RCOMP_1:def 2;
].(b - g),(b + g).[ c= [.a,b.] by A1, A9;
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 ex l being Real st
( l = b + (g / 2) & a <= l & l <= b ) ;
hence contradiction by A10; :: thesis: verum

end;

end;