theorem :: TOPALG_1:54

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) " = pi_1-iso (- R) by Th53, BORSUK_2:def 3;