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:52;
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:52;
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:30
.= 1 by A1 ;
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:8;
A6: dom (Sq_Circ | Kb) = (dom Sq_Circ) /\ Kb by RELAT_1:61
.= 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 object ; :: 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 object st
( z in dom (Sq_Circ | Kb) & u = (Sq_Circ | Kb) . z ) by FUNCT_1:def 3;
hence u in (Sq_Circ | Kb) .: the carrier of ((TOP-REAL 2) | Kb) by A6, FUNCT_1:def 6; :: thesis: verum

end;

(Sq_Circ | Kb) .: the carrier of ((TOP-REAL 2) | Kb) = Sq_Circ .: Kb by A5, RELAT_1:129
.= Cb by A3, Th23
.= the carrier of ((TOP-REAL 2) | Cbb) by PRE_TOPC:8 ;
then reconsider f0 = Sq_Circ | Kb as Function of ((TOP-REAL 2) | Kb),((TOP-REAL 2) | Cbb) by A6, A7, FUNCT_2:2;
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:2;
A8: ( f0 is one-to-one & Kb is compact ) by Th25, FUNCT_1:52;
rng f0 = (Sq_Circ | Kb) .: the carrier of ((TOP-REAL 2) | Kb) by RELSET_1:22
.= Sq_Circ .: Kb by A5, RELAT_1:129
.= Cb by A3, Th23 ;
then ex f1 being Function of ((TOP-REAL 2) | Kb),((TOP-REAL 2) | Cbb) st
( f00 = f1 & f1 is being_homeomorphism ) by A8, Th21, JGRAPH_1:46, TOPMETR:7;
hence Cb is being_simple_closed_curve by Th24; :: thesis: verum