theorem :: TOPALG_5:6

for S, T being TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is connected holds
T is connected