let S, T be non empty TopSpace; :: thesis: ( S,T are_homeomorphic & S is compact implies T is compact )
assume A1: ( S,T are_homeomorphic & S is compact ) ; :: thesis: T is compact
then consider f being Function of S,T such that
A2: f is being_homeomorphism by T_0TOPSP:def 1;
( f is continuous & rng f = [#] T ) by A2, TOPS_2:def 5;
hence T is compact by A1, COMPTS_1:23; :: thesis: verum