let X be non empty TopSpace; :: thesis: for Y being non empty SubSpace of X
for x1, x2 being Point of X
for y1, y2 being Point of Y
for f being Path of x1,x2 st x1 = y1 & x2 = y2 & x1,x2 are_connected & rng f c= the carrier of Y holds
( y1,y2 are_connected & f is Path of y1,y2 )
let Y be non empty SubSpace of X; :: thesis: for x1, x2 being Point of X
for y1, y2 being Point of Y
for f being Path of x1,x2 st x1 = y1 & x2 = y2 & x1,x2 are_connected & rng f c= the carrier of Y holds
( y1,y2 are_connected & f is Path of y1,y2 )
let x1, x2 be Point of X; :: thesis: for y1, y2 being Point of Y
for f being Path of x1,x2 st x1 = y1 & x2 = y2 & x1,x2 are_connected & rng f c= the carrier of Y holds
( y1,y2 are_connected & f is Path of y1,y2 )
let y1, y2 be Point of Y; :: thesis: for f being Path of x1,x2 st x1 = y1 & x2 = y2 & x1,x2 are_connected & rng f c= the carrier of Y holds
( y1,y2 are_connected & f is Path of y1,y2 )
let f be Path of x1,x2; :: thesis: ( x1 = y1 & x2 = y2 & x1,x2 are_connected & rng f c= the carrier of Y implies ( y1,y2 are_connected & f is Path of y1,y2 ) )
assume that
A1: ( x1 = y1 & x2 = y2 ) and
A2: x1,x2 are_connected ; :: thesis: ( not rng f c= the carrier of Y or ( y1,y2 are_connected & f is Path of y1,y2 ) )
assume rng f c= the carrier of Y ; :: thesis: ( y1,y2 are_connected & f is Path of y1,y2 )
then reconsider g = f as Function of I[01] ,Y by FUNCT_2:8;
A3: f is continuous by A2, BORSUK_2:def 2;
thus A4: ex f being Function of I[01] ,Y st
( f is continuous & f . 0 = y1 & f . 1 = y2 ) :: according to BORSUK_2:def 1 :: thesis: f is Path of y1,y2

proof

take g ; :: thesis: ( g is continuous & g . 0 = y1 & g . 1 = y2 )
thus g is continuous by A3, PRE_TOPC:57; :: thesis: ( g . 0 = y1 & g . 1 = y2 )
thus ( g . 0 = y1 & g . 1 = y2 ) by A1, A2, BORSUK_2:def 2; :: thesis: verum

end;

g is Path of y1,y2

proof

thus ex f being Function of I[01] ,Y st
( f is continuous & f . 0 = y1 & f . 1 = y2 ) by A4; :: according to BORSUK_2:def 1,BORSUK_2:def 2 :: thesis: ( g is continuous & g . 0 = y1 & g . 1 = y2 )
thus g is continuous by A3, PRE_TOPC:57; :: thesis: ( g . 0 = y1 & g . 1 = y2 )
thus ( g . 0 = y1 & g . 1 = y2 ) by A1, A2, BORSUK_2:def 2; :: thesis: verum

end;

hence f is Path of y1,y2 ; :: thesis: verum