let GX be non empty TopSpace; ( GX is pathwise_connected implies GX is connected )
assume A1:
for x, y being Point of GX holds x,y are_connected
; BORSUK_2:def 3 GX is connected
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 ) )
proof
let x,
y be
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 ) )
x,
y are_connected
by A1;
then consider h being
Function of
I[01],
GX such that A2:
h is
continuous
and A3:
x = h . 0
and A4:
y = h . 1
;
1
in dom h
by Lm2, BORSUK_1:40, FUNCT_2:def 1;
then A5:
y in rng h
by A4, FUNCT_1:def 3;
0 in dom h
by Lm2, BORSUK_1:40, FUNCT_2:def 1;
then
x in rng h
by A3, FUNCT_1:def 3;
hence
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 ) )
by A2, A5, TREAL_1:19;
verum
end;
hence
GX is connected
by TOPS_2:63; verum