theorem :: BORSUK_6:78

for X being non empty pathwise_connected TopSpace
for a1, b1 being Point of X
for P, Q being Path of a1,b1 st P,Q are_homotopic holds
- P, - Q are_homotopic by Th77, BORSUK_2:def 3;