let A be Subset of R^1; :: thesis: for a being Real st not a in A & ex b, d being Real st
( b in A & d in A & b < a & a < d ) holds
not A is connected
let a be Real; :: thesis: ( not a in A & ex b, d being Real 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 st
( b in A & d in A & b < a & a < d ) ; :: thesis: not A is connected
consider b, d being Real 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 Real : s > a } ;
set B1 = { r where r is Real : r < a } ;
A7: A c= { r where r is Real : r < a } \/ { s where s is Real : s > a }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in { r where r is Real : r < a } \/ { s where s is Real : s > a } )
assume A8: x in A ; :: thesis: x in { r where r is Real : r < a } \/ { s where s is Real : s > a }
then reconsider r = x as Real ;
( r < a or a < r ) by A1, A8, XXREAL_0:1;
then ( r in { r where r is Real : r < a } or r in { s where s is Real : s > a } ) ;
hence x in { r where r is Real : r < a } \/ { s where s is Real : s > a } by XBOOLE_0:def 3; :: thesis: verum

end;

{ s where s is Real : s > a } c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Real : s > a } or x in REAL )
assume x in { s where s is Real : s > a } ; :: thesis: x in REAL
then consider r being Real such that
A9: r = x and
r > a ;
r in REAL by XREAL_0:def 1;
hence x in REAL by A9; :: thesis: verum

end;

then reconsider C2 = { s where s is Real : s > a } as Subset of R^1 by METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6;
{ r where r is Real : r < a } c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { r where r is Real : r < a } or x in REAL )
assume x in { r where r is Real : r < a } ; :: thesis: x in REAL
then consider r being Real such that
A10: r = x and
r < a ;
r in REAL by XREAL_0:def 1;
hence x in REAL by A10; :: thesis: verum

end;

then reconsider C1 = { r where r is Real : r < a } as Subset of R^1 by METRIC_1:def 13, TOPMETR:12, TOPMETR:def 6;

A11: now :: thesis: not { r where r is Real : r < a } meets { s where s is Real : s > a }

assume { r where r is Real : r < a } meets { s where s is Real : s > a } ; :: thesis: contradiction
then consider x being object such that
A12: x in { r where r is Real : r < a } /\ { s where s is Real : s > a } by XBOOLE_0:4;
x in { s where s is Real : s > a } by A12, XBOOLE_0:def 4;
then A13: ex r2 being Real st
( r2 = x & r2 > a ) ;
x in { r where r is Real : r < a } by A12, XBOOLE_0:def 4;
then ex r1 being Real st
( r1 = x & r1 < a ) ;
hence contradiction by A13; :: thesis: verum

end;

reconsider r1 = d as Element of REAL by XREAL_0:def 1;
r1 in { s where s is Real : s > a } by A6;
then d in { s where s is Real : s > a } /\ A by A4, XBOOLE_0:def 4;
then A14: { s where s is 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 Real : r < a } by A5;
then b in { r where r is Real : r < a } /\ A by A3, XBOOLE_0:def 4;
then A15: { r where r is 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 A11, A15, A14, A7, Th1; :: thesis: verum