theorem :: TOPALG_3:8
for T being TopSpace st TopStruct(# the carrier of T, the topology of T #) is connected holds
T is connected