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