let GX be non empty TopSpace; :: thesis: ( GX is pathwise_connected implies GX is connected )
assume A1: for x, y being Point of GX holds x,y are_connected ; :: according to BORSUK_2:def 3 :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

hence GX is connected by TOPS_2:63; :: thesis: verum