for T being non empty pathwise_connected TopSpace
for y0, y1 being Point of T
for R being Path of y0,y1 holds pi_1-iso R is bijective ;