:: deftheorem Def2 defines Path BORSUK_2:def 2 :
for T being TopStruct
for a, b being Point of T st a,b are_connected holds
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 ) );