let X be non empty arcwise_connected TopSpace; :: thesis: for a1, b1, c1, d1 being Point of X
for P being Path of a1,b1
for Q being Path of b1,c1
for R being Path of c1,d1 holds (P + Q) + R,P + (Q + R) are_homotopic
let a1, b1, c1, d1 be Point of X; :: thesis: for P being Path of a1,b1
for Q being Path of b1,c1
for R being Path of c1,d1 holds (P + Q) + R,P + (Q + R) are_homotopic
let P be Path of a1,b1; :: thesis: for Q being Path of b1,c1
for R being Path of c1,d1 holds (P + Q) + R,P + (Q + R) are_homotopic
let Q be Path of b1,c1; :: thesis: for R being Path of c1,d1 holds (P + Q) + R,P + (Q + R) are_homotopic
let R be Path of c1,d1; :: thesis: (P + Q) + R,P + (Q + R) are_homotopic
( a1,b1 are_connected & b1,c1 are_connected & c1,d1 are_connected ) by BORSUK_2:def 3;
hence (P + Q) + R,P + (Q + R) are_homotopic by Th81; :: thesis: verum