let S, T be non empty TopSpace; :: thesis: ( S,T are_homeomorphic & S is compact implies T is compact )
assume that
A1: S,T are_homeomorphic and
A2: S is compact ; :: thesis: T is compact
consider f being Function of S,T such that
A3: f is being_homeomorphism by A1;
( f is continuous & rng f = [#] T ) by A3;
hence T is compact by A2, COMPTS_1:14; :: thesis: verum