:: deftheorem Def5 defines + BORSUK_2:def 5 :
for T being non empty TopSpace
for a, b, c being Point of T
for P being Path of a,b
for Q being Path of b,c st a,b are_connected & b,c are_connected holds
for b₇ being Path of a,c holds
( b₇ = P + Q iff for t being Point of I[01] holds
( ( t <= 1 / 2 implies b₇ . t = P . (2 * t) ) & ( 1 / 2 <= t implies b₇ . t = Q . ((2 * t) - 1) ) ) );