let GX be non empty TopSpace; :: thesis: ( GX is arcwise_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 ) )

now

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 & y = h . 1 ) by Def1;
( 0 in dom h & 1 in dom h ) by Lm2, BORSUK_1:83, FUNCT_2:def 1;
then ( x in rng h & y in rng h ) by A3, FUNCT_1:def 5;
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, TREAL_1:22; :: thesis: verum

end;

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 ) ) ; :: thesis: verum

end;

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