set v = |[1,0]|;
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 )
( |[1,0]| `1 = 1 & |[1,0]| `2 = 0 ) by EUCLID:52;
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;
set P = Kb;
id ((TOP-REAL 2) | Kbd) is being_homeomorphism ;
hence Kb is being_simple_closed_curve by A1, Th24; :: thesis: Kb is compact
then consider f being Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | Kb) such that
A2: f is being_homeomorphism by TOPREAL2:def 1;

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

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

Kbd <> {} ;
hence Kb is compact by A3; :: 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 A2, TOPS_2:def 5;
then (TOP-REAL 2) | R is compact by COMPTS_1:14;
hence Kb is compact by COMPTS_1:3; :: thesis: verum

end;

end;