let T be non empty arcwise_connected TopSpace; :: thesis: for a, b being Point of T
for A being Path of a,b holds A = - (- A)
let a, b be Point of T; :: thesis: for A being Path of a,b holds A = - (- A)
a,b are_connected by BORSUK_2:def 3;
hence for A being Path of a,b holds A = - (- A) by Th50; :: thesis: verum