let T be non empty arcwise_connected TopSpace; :: thesis: for a1, b1, d1, c1 being Point of T
for A being Path of a1,b1
for B being Path of d1,b1
for C being Path of b1,c1 holds ((A + (- B)) + B) + C,A + C are_homotopic
let a1, b1, d1, c1 be Point of T; :: thesis: for A being Path of a1,b1
for B being Path of d1,b1
for C being Path of b1,c1 holds ((A + (- B)) + B) + C,A + C are_homotopic
( a1,b1 are_connected & b1,c1 are_connected & b1,d1 are_connected ) by BORSUK_2:def 3;
hence for A being Path of a1,b1
for B being Path of d1,b1
for C being Path of b1,c1 holds ((A + (- B)) + B) + C,A + C are_homotopic by Th38; :: thesis: verum