let T be non empty pathwise_connected TopSpace; :: thesis: for y0, y1 being Point of T
for R being Path of y0,y1 holds (pi_1-iso R) " = pi_1-iso (- R)
let y0, y1 be Point of T; :: thesis: for R being Path of y0,y1 holds (pi_1-iso R) " = pi_1-iso (- R)
let R be Path of y0,y1; :: thesis: (pi_1-iso R) " = pi_1-iso (- R)
y0,y1 are_connected by BORSUK_2:def 3;
hence (pi_1-iso R) " = pi_1-iso (- R) by Th54; :: thesis: verum