:: deftheorem Def3 defines - BORSUK_6:def 3 :
for T being non empty pathwise_connected TopSpace
for a, b being Point of T
for P being Path of a,b
for b₅ being Path of b,a holds
( b₅ = - P iff for t being Point of I[01] holds b₅ . t = P . (1 - t) );