for X being non empty TopSpace
for a, b, c, d being Point of X st a,b are_connected & a,c are_connected & c,d are_connected holds
for A being Path of a,b
for B being Path of c,d
for C being Path of a,c holds (((A + (- A)) + C) + B) + (- B),C are_homotopic