let A be Subset of R^1 ; :: thesis: for a being real number st not a in A & ex b, d being real number st
( b in A & d in A & b < a & a < d ) holds
not A is connected
let a be real number ; :: thesis: ( not a in A & ex b, d being real number st
( b in A & d in A & b < a & a < d ) implies not A is connected )
assume A1: ( not a in A & ex b, d being real number st
( b in A & d in A & b < a & a < d ) ) ; :: thesis: not A is connected
then consider b, d being real number such that
A2: ( b in A & d in A & b < a & a < d ) ;
set B1 = { r where r is Element of REAL : r < a } ;
set B2 = { s where s is Element of REAL : s > a } ;

A3: now

assume { r where r is Element of REAL : r < a } meets { s where s is Element of REAL : s > a } ; :: thesis: contradiction
then consider x being set such that
A4: x in { r where r is Element of REAL : r < a } /\ { s where s is Element of REAL : s > a } by XBOOLE_0:4;
x in { r where r is Element of REAL : r < a } by A4, XBOOLE_0:def 4;
then consider r1 being Element of REAL such that
A5: ( r1 = x & r1 < a ) ;
x in { s where s is Element of REAL : s > a } by A4, XBOOLE_0:def 4;
then consider r2 being Element of REAL such that
A6: ( r2 = x & r2 > a ) ;
thus contradiction by A5, A6; :: thesis: verum

end;

reconsider r = b as Element of REAL by XREAL_0:def 1;
r in { r where r is Element of REAL : r < a } by A2;
then b in { r where r is Element of REAL : r < a } /\ A by A2, XBOOLE_0:def 4;
then A7: { r where r is Element of REAL : r < a } meets A by XBOOLE_0:4;
reconsider r1 = d as Element of REAL by XREAL_0:def 1;
r1 in { s where s is Element of REAL : s > a } by A2;
then d in { s where s is Element of REAL : s > a } /\ A by A2, XBOOLE_0:def 4;
then A8: { s where s is Element of REAL : s > a } meets A by XBOOLE_0:4;
A9: A c= { r where r is Element of REAL : r < a } \/ { s where s is Element of REAL : s > a }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in { r where r is Element of REAL : r < a } \/ { s where s is Element of REAL : s > a } )
assume A10: x in A ; :: thesis: x in { r where r is Element of REAL : r < a } \/ { s where s is Element of REAL : s > a }
then reconsider r = x as Real by METRIC_1:def 14, TOPMETR:16, TOPMETR:def 7;
( r < a or a < r ) by A1, A10, XXREAL_0:1;
then ( r in { r where r is Element of REAL : r < a } or r in { s where s is Element of REAL : s > a } ) ;
hence x in { r where r is Element of REAL : r < a } \/ { s where s is Element of REAL : s > a } by XBOOLE_0:def 3; :: thesis: verum

end;

{ r where r is Element of REAL : r < a } c= REAL

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { r where r is Element of REAL : r < a } or x in REAL )
assume x in { r where r is Element of REAL : r < a } ; :: thesis: x in REAL
then ex r being Element of REAL st
( r = x & r < a ) ;
hence x in REAL ; :: thesis: verum

end;

then reconsider C1 = { r where r is Element of REAL : r < a } as Subset of R^1 by METRIC_1:def 14, TOPMETR:16, TOPMETR:def 7;
A11: C1 is open by JORDAN2B:30;
{ s where s is Element of REAL : s > a } c= REAL

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Element of REAL : s > a } or x in REAL )
assume x in { s where s is Element of REAL : s > a } ; :: thesis: x in REAL
then ex r being Element of REAL st
( r = x & r > a ) ;
hence x in REAL ; :: thesis: verum

end;

then reconsider C2 = { s where s is Element of REAL : s > a } as Subset of R^1 by METRIC_1:def 14, TOPMETR:16, TOPMETR:def 7;
C2 is open by JORDAN2B:31;
hence not A is connected by A3, A7, A8, A9, A11, Th4; :: thesis: verum