theorem :: TOPALG_1:38

for T being non empty pathwise_connected TopSpace
for a1, b1, c1, d1 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