let P be Subset of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve implies ( not P is empty & P is compact ) )

given f being Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | P) such that A1: f is being_homeomorphism ; :: according to TOPREAL2:def 1 :: thesis: ( not P is empty & P is compact )

thus not P is empty by A1, Lm37; :: thesis: P is compact

A2: rng f = [#] ((TOP-REAL 2) | P) by A1;

reconsider R = P as non empty Subset of (TOP-REAL 2) by A1, Lm37;

A3: f is continuous by A1;

(TOP-REAL 2) | R^2-unit_square is compact by Th2, COMPTS_1:3;

then (TOP-REAL 2) | R is compact by A3, A2, COMPTS_1:14;

hence P is compact by COMPTS_1:3; :: thesis: verum

given f being Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | P) such that A1: f is being_homeomorphism ; :: according to TOPREAL2:def 1 :: thesis: ( not P is empty & P is compact )

thus not P is empty by A1, Lm37; :: thesis: P is compact

A2: rng f = [#] ((TOP-REAL 2) | P) by A1;

reconsider R = P as non empty Subset of (TOP-REAL 2) by A1, Lm37;

A3: f is continuous by A1;

(TOP-REAL 2) | R^2-unit_square is compact by Th2, COMPTS_1:3;

then (TOP-REAL 2) | R is compact by A3, A2, COMPTS_1:14;

hence P is compact by COMPTS_1:3; :: thesis: verum