let X be open Subset of REAL; for a, b being Real st X c= [.a,b.] holds
( not a in X & not b in X )
let a, b be Real; ( X c= [.a,b.] implies ( not a in X & not b in X ) )
assume A1:
X c= [.a,b.]
; ( not a in X & not b in X )
assume A2:
( a in X or b in X )
; contradiction
per cases
( a in X or b in X )
by A2;
suppose
a in X
;
contradictionthen 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;
verum end; suppose
b in X
;
contradictionthen 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;
verum end;