defpred S₁[ Point of (TOP-REAL 2)] means ( ( - 1 = $1 `1 & - 1 <= $1 `2 & $1 `2 <= 1 ) or ( $1 `1 = 1 & - 1 <= $1 `2 & $1 `2 <= 1 ) or ( - 1 = $1 `2 & - 1 <= $1 `1 & $1 `1 <= 1 ) or ( 1 = $1 `2 & - 1 <= $1 `1 & $1 `1 <= 1 ) );
A1: ( |[1,0 ]| `1 = 1 & |[1,0 ]| `2 = 0 ) by EUCLID:56;
A2: dom Sq_Circ = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
set v = |[1,0 ]|;
let Cb be Subset of (TOP-REAL 2); :: thesis: ( Cb = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } implies Cb is being_simple_closed_curve )
assume A3: Cb = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } ; :: thesis: Cb is being_simple_closed_curve
( |[1,0 ]| `1 = 1 & |[1,0 ]| `2 = 0 ) by EUCLID:56;
then A4: |[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 ) ) } ;
{ q where q is Element of (TOP-REAL 2) : S₁[q] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
then reconsider 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 ) ) } as non empty Subset of (TOP-REAL 2) by A4;
|.|[1,0 ]|.| = sqrt (((|[1,0 ]| `1 ) ^2 ) + ((|[1,0 ]| `2 ) ^2 )) by JGRAPH_1:47
.= 1 by A1, SQUARE_1:83 ;
then |[1,0 ]| in Cb by A3;
then reconsider Cbb = Cb as non empty Subset of (TOP-REAL 2) ;
A5: the carrier of ((TOP-REAL 2) | Kb) = Kb by PRE_TOPC:29;
A6: dom (Sq_Circ | Kb) = (dom Sq_Circ ) /\ Kb by RELAT_1:90
.= the carrier of ((TOP-REAL 2) | Kb) by A5, A2, XBOOLE_1:28 ;
A7: rng (Sq_Circ | Kb) c= (Sq_Circ | Kb) .: the carrier of ((TOP-REAL 2) | Kb)

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in rng (Sq_Circ | Kb) or u in (Sq_Circ | Kb) .: the carrier of ((TOP-REAL 2) | Kb) )
assume u in rng (Sq_Circ | Kb) ; :: thesis: u in (Sq_Circ | Kb) .: the carrier of ((TOP-REAL 2) | Kb)
then ex z being set st
( z in dom (Sq_Circ | Kb) & u = (Sq_Circ | Kb) . z ) by FUNCT_1:def 5;
hence u in (Sq_Circ | Kb) .: the carrier of ((TOP-REAL 2) | Kb) by A6, FUNCT_1:def 12; :: thesis: verum

end;

(Sq_Circ | Kb) .: the carrier of ((TOP-REAL 2) | Kb) = Sq_Circ .: Kb by A5, RELAT_1:162
.= Cb by A3, Th33
.= the carrier of ((TOP-REAL 2) | Cbb) by PRE_TOPC:29 ;
then reconsider f0 = Sq_Circ | Kb as Function of ((TOP-REAL 2) | Kb),((TOP-REAL 2) | Cbb) by A6, A7, FUNCT_2:4;
rng (Sq_Circ | Kb) c= the carrier of (TOP-REAL 2) ;
then reconsider f00 = f0 as Function of ((TOP-REAL 2) | Kb),(TOP-REAL 2) by A6, FUNCT_2:4;
A8: ( f0 is one-to-one & Kb is compact ) by Th35, FUNCT_1:84;
rng f0 = (Sq_Circ | Kb) .: the carrier of ((TOP-REAL 2) | Kb) by FUNCT_2:45
.= Sq_Circ .: Kb by A5, RELAT_1:162
.= Cb by A3, Th33 ;
then ex f1 being Function of ((TOP-REAL 2) | Kb),((TOP-REAL 2) | Cbb) st
( f00 = f1 & f1 is being_homeomorphism ) by A8, Th31, JGRAPH_1:64, TOPMETR:10;
hence Cb is being_simple_closed_curve by Th34; :: thesis: verum