set v = |[1,0]|;
let Kb be Subset of (); :: thesis: ( Kb = { q where q is Point of () : ( ( - 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 () : ( ( - 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 () : ( ( - 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 () by A1;
set P = Kb;
id (() | Kbd) is being_homeomorphism ;
hence Kb is being_simple_closed_curve by ; :: thesis: Kb is compact
then consider f being Function of (),(() | Kb) such that
A2: f is being_homeomorphism by TOPREAL2:def 1;
per cases ( Kb is empty or not Kb is empty ) ;
end;