let Kb be Subset of (TOP-REAL 2); :: thesis: ( Kb = { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } implies ( Kb is being_simple_closed_curve & Kb is compact ) )
assume A1: Kb = { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } ; :: thesis: ( Kb is being_simple_closed_curve & Kb is compact )
set v = |[1,0 ]|;
( |[1,0 ]| `1 = 1 & |[1,0 ]| `2 = 0 ) by EUCLID:56;
then |[1,0 ]| in { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } ;
then reconsider Kbd = Kb as non empty Subset of (TOP-REAL 2) by A1;
id ((TOP-REAL 2) | Kbd) is being_homeomorphism ;
hence A2: Kb is being_simple_closed_curve by A1, Th34; :: thesis: Kb is compact
set P = Kb;
consider f being Function of ((TOP-REAL 2) | R^2-unit_square ),((TOP-REAL 2) | Kb) such that
A3: f is being_homeomorphism by A2, TOPREAL2:def 1;

per cases ( Kb is empty or not Kb is empty ) ;

suppose A4: Kb is empty ; :: thesis: Kb is compact

Kbd <> {} ;
hence Kb is compact by A4; :: thesis: verum

end;

suppose not Kb is empty ; :: thesis: Kb is compact

then reconsider R = Kb as non empty Subset of (TOP-REAL 2) ;
( f is continuous & rng f = [#] ((TOP-REAL 2) | Kb) ) by A3, TOPS_2:def 5;
then (TOP-REAL 2) | R is compact by COMPTS_1:23;
hence Kb is compact by COMPTS_1:12; :: thesis: verum

end;

end;