for X being non empty TopSpace
for x0, x1 being Point of X
for P being Path of x0,x1 st x0,x1 are_connected holds
pi_1-iso P is one-to-one