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;

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 )
;

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;( 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