let GX be non empty TopSpace; ( ( for x, y being Point of GX ex GY being non empty TopSpace st
( GY is connected & ex f being Function of GY,GX st
( f is continuous & x in rng f & y in rng f ) ) ) implies GX is connected )
assume A1:
for x, y being Point of GX ex GY being non empty TopSpace st
( GY is connected & ex f being Function of GY,GX st
( f is continuous & x in rng f & y in rng f ) )
; GX is connected
for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open holds
A meets B
proof
let A,
B be
Subset of
GX;
( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open implies A meets B )
assume that A2:
[#] GX = A \/ B
and A3:
A <> {} GX
and A4:
B <> {} GX
and A5:
(
A is
open &
B is
open )
;
A meets B
set v = the
Element of
B;
set u = the
Element of
A;
reconsider y = the
Element of
B as
Point of
GX by A2, A4, XBOOLE_0:def 3;
reconsider x = the
Element of
A as
Point of
GX by A2, A3, XBOOLE_0:def 3;
consider GY being non
empty TopSpace such that A6:
GY is
connected
and A7:
ex
f being
Function of
GY,
GX st
(
f is
continuous &
x in rng f &
y in rng f )
by A1;
consider f being
Function of
GY,
GX such that A8:
f is
continuous
and A9:
x in rng f
and A10:
y in rng f
by A7;
f " ([#] GX) = [#] GY
by Th41;
then A11:
(f " A) \/ (f " B) = [#] GY
by A2, RELAT_1:140;
(rng f) /\ B <> {}
by A4, A10, XBOOLE_0:def 4;
then
rng f meets B
by XBOOLE_0:def 7;
then A12:
f " B <> {} GY
by RELAT_1:138;
(rng f) /\ A <> {}
by A3, A9, XBOOLE_0:def 4;
then
rng f meets A
by XBOOLE_0:def 7;
then A13:
f " A <> {} GY
by RELAT_1:138;
[#] GX <> {}
;
then
(
f " A is
open &
f " B is
open )
by A5, A8, Th43;
then
f " A meets f " B
by A6, A11, A13, A12, CONNSP_1:11;
then
(f " A) /\ (f " B) <> {}
by XBOOLE_0:def 7;
then
f " (A /\ B) <> {}
by FUNCT_1:68;
then
rng f meets A /\ B
by RELAT_1:138;
then
ex
u1 being
object st
(
u1 in rng f &
u1 in A /\ B )
by XBOOLE_0:3;
hence
A meets B
by XBOOLE_0:4;
verum
end;
hence
GX is connected
by CONNSP_1:11; verum