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 y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds
f is Path of x1,x2
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 y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds
f is Path of x1,x2
let x1, x2 be Point of X; :: thesis: for y1, y2 being Point of Y
for f being Path of y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds
f is Path of x1,x2
let y1, y2 be Point of Y; :: thesis: for f being Path of y1,y2 st x1 = y1 & x2 = y2 & y1,y2 are_connected holds
f is Path of x1,x2
let f be Path of y1,y2; :: thesis: ( x1 = y1 & x2 = y2 & y1,y2 are_connected implies f is Path of x1,x2 )
assume that
A1: ( x1 = y1 & x2 = y2 ) and
A2: y1,y2 are_connected ; :: thesis: f is Path of x1,x2
the carrier of Y is Subset of X by TSEP_1:1;
then reconsider g = f as Function of I[01],X by FUNCT_2:7;
f is continuous by A2, BORSUK_2:def 2;
then A3: g is continuous by PRE_TOPC:26;
A4: ( g . 0 = x1 & g . 1 = x2 ) by A1, A2, BORSUK_2:def 2;
then x1,x2 are_connected by A3;
hence f is Path of x1,x2 by A4, A3, BORSUK_2:def 2; :: thesis: verum