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 )
A2: (TOP-REAL 2) | R^2-unit_square is compact by Th2, COMPTS_1:12;
thus not P is empty by A1, Lm30, PRE_TOPC:def 10; :: thesis: P is compact
then reconsider R = P as non empty Subset of (TOP-REAL 2) ;
( f is continuous & rng f = [#] ((TOP-REAL 2) | P) ) by A1, TOPS_2:def 5;
then (TOP-REAL 2) | R is compact by A2, COMPTS_1:23;
hence P is compact by COMPTS_1:12; :: thesis: verum