for X being 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 )