for T being non empty TopSpace
for a, b, c, d being Point of T
for P being Path of a,b
for Q being Path of b,c
for R being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds
(P + Q) + R,P + (Q + R) are_homotopic