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