let X be Path of b,a; :: thesis: ( X = - P iff for t being Point of I[01] holds X . t = P . (1 - t) )
b,a are_connected by BORSUK_2:def 3;
hence ( X = - P iff for t being Point of I[01] holds X . t = P . (1 - t) ) by BORSUK_2:def 6; :: thesis: verum