let GX be non empty TopSpace; :: thesis: ( ( for x, y being Point of GX ex h being Function of I[01],GX st
( h is continuous & x = h . 0 & y = h . 1 ) ) implies GX is connected )
assume A1: for x, y being Point of GX ex h being Function of I[01],GX st
( h is continuous & x = h . 0 & y = h . 1 ) ; :: 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 :: 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 ) )

consider h being Function of I[01],GX such that
A2: h is continuous and
A3: x = h . 0 and
A4: y = h . 1 by A1;
A5: 0 in dom h by Lm1, BORSUK_1:40, FUNCT_2:def 1;
A6: 1 in dom h by Lm1, BORSUK_1:40, FUNCT_2:def 1;
A7: x in rng h by A3, A5, FUNCT_1:def 3;
y in rng h by A4, A6, 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, A7, TREAL_1:19; :: 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:63; :: thesis: verum