let A be Subset of R^1; 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; ( 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 )
; 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 }
{ s where s is Real : s > a } c= REAL
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
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;
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; verum