:: deftheorem Def4 defines Path BORSUK_2:def 4 :
for T being pathwise_connected TopStruct
for a, b being Point of T
for b₄ being Function of I[01],T holds
( b₄ is Path of a,b iff ( b₄ is continuous & b₄ . 0 = a & b₄ . 1 = b ) );