let S, T be TopSpace; :: thesis: ( S,T are_homeomorphic & S is connected implies T is connected )
given f being Function of S,T such that A1: f is being_homeomorphism ; :: according to T_0TOPSP:def 1 :: thesis: ( not S is connected or T is connected )
assume A2: S is connected ; :: thesis: T is connected
A3: f is continuous by A1;
( dom f = [#] S & rng f = [#] T ) by A1, TOPS_2:def 5;
then f .: ([#] S) = [#] T by RELAT_1:146;
hence T is connected by A2, A3, CONNSP_1:15; :: thesis: verum