let X be non empty TopSpace; 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; 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; 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; 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; ( 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
and
A2:
x2 = y2
and
A3:
x1,x2 are_connected
; ( 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
; ( y1,y2 are_connected & f is Path of y1,y2 )
then reconsider g = f as Function of I[01],Y by FUNCT_2:6;
A4:
f is continuous
by A3, BORSUK_2:def 2;
A5:
( f . 0 = y1 & f . 1 = y2 )
by A1, A2, A3, BORSUK_2:def 2;
A6:
g is continuous
by A4, PRE_TOPC:27;
thus
ex f being Function of I[01],Y st
( f is continuous & f . 0 = y1 & f . 1 = y2 )
BORSUK_2:def 1 f is Path of y1,y2
y1,y2 are_connected
by A5, A6;
hence
f is Path of y1,y2
by A5, A6, BORSUK_2:def 2; verum