theorem Th19: :: TOPALG_1:19
for X being non empty TopSpace
for a, b, c being Point of X st a,b are_connected & b,c are_connected holds
for A1, A2 being Path of a,b
for B being Path of b,c st A1,A2 are_homotopic holds
A1,(A2 + B) + (- B) are_homotopic