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