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 that
A1: not a in A and
A2: ex b, d being real number st
( b in A & d in A & b < a & a < d ) ; :: thesis: not A is connected
consider b, d being real number such that
A3: b in A and
A4: d in A and
A5: b < a and
A6: a < d by A2;
set B2 = { s where s is Element of REAL : s > a } ;
set B1 = { r where r is Element of REAL : r < a } ;
A7: 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 A8: 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 13, TOPMETR:12, TOPMETR:def 6;
( r < a or a < r ) by A1, A8, 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;

{ 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 13, TOPMETR:12, TOPMETR:def 6;
{ 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 13, TOPMETR:12, TOPMETR:def 6;

A9: 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
A10: 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 { s where s is Element of REAL : s > a } by A10, XBOOLE_0:def 4;
then A11: ex r2 being Element of REAL st
( r2 = x & r2 > a ) ;
x in { r where r is Element of REAL : r < a } by A10, XBOOLE_0:def 4;
then ex r1 being Element of REAL st
( r1 = x & r1 < a ) ;
hence contradiction by A11; :: thesis: verum

end;

reconsider r1 = d as Element of REAL by XREAL_0:def 1;
r1 in { s where s is Element of REAL : s > a } by A6;
then d in { s where s is Element of REAL : s > a } /\ A by A4, XBOOLE_0:def 4;
then A12: { s where s is Element of REAL : s > a } meets A by XBOOLE_0:4;
reconsider r = b as Element of REAL by XREAL_0:def 1;
r in { r where r is Element of REAL : r < a } by A5;
then b in { r where r is Element of REAL : r < a } /\ A by A3, XBOOLE_0:def 4;
then A13: { r where r is Element of REAL : r < a } meets A by XBOOLE_0:4;
( C1 is open & C2 is open ) by JORDAN2B:24, JORDAN2B:25;
hence not A is connected by A9, A13, A12, A7, Th4; :: thesis: verum