:: deftheorem defines are_connected BORSUK_2:def 1 :
for T being TopStruct
for a, b being Point of T holds
( a,b are_connected iff ex f being Function of I[01],T st
( f is continuous & f . 0 = a & f . 1 = b ) );