:: deftheorem defines + BORSUK_6:def 2 :
for T being non empty pathwise_connected TopSpace
for a, b, c being Point of T
for P being Path of a,b
for Q being Path of b,c
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) ) ) );