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 ) )

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

hence
GX is connected
by TOPS_2:63; :: thesis: verum
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;( 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