let a, b, r be real number ; :: thesis: for Cb being Subset of (TOP-REAL 2) st r > 0 & Cb = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } holds
Cb is being_simple_closed_curve
let Cb be Subset of (TOP-REAL 2); :: thesis: ( r > 0 & Cb = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } implies Cb is being_simple_closed_curve )
assume A1: ( r > 0 & Cb = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } ) ; :: thesis: Cb is being_simple_closed_curve
A2: ( |[r,0 ]| `1 = r & |[r,0 ]| `2 = 0 ) by EUCLID:56;
|.(|[(r + a),b]| - |[a,b]|).| = |.(|[(r + a),(0 + b)]| - |[a,b]|).|
.= |.((|[r,0 ]| + |[a,b]|) - |[a,b]|).| by EUCLID:60
.= |.(|[r,0 ]| + (|[a,b]| - |[a,b]|)).| by EUCLID:49
.= |.(|[r,0 ]| + (0. (TOP-REAL 2))).| by EUCLID:46
.= |.|[r,0 ]|.| by EUCLID:31
.= sqrt ((r ^2 ) + (0 ^2 )) by A2, JGRAPH_3:10
.= r by A1, SQUARE_1:89 ;
then |[(r + a),b]| in Cb by A1;
then reconsider Cbb = Cb as non empty Subset of (TOP-REAL 2) ;
set v = |[1,0 ]|;
( |[1,0 ]| `1 = 1 & |[1,0 ]| `2 = 0 ) by EUCLID:56;
then |.|[1,0 ]|.| = sqrt ((1 ^2 ) + (0 ^2 )) by JGRAPH_3:10
.= 1 by SQUARE_1:89 ;
then A3: |[1,0 ]| in { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } ;
defpred S₁[ Point of (TOP-REAL 2)] means |.$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) : |.q.| = 1 } as non empty Subset of (TOP-REAL 2) by A3;
A4: the carrier of ((TOP-REAL 2) | Kb) = Kb by PRE_TOPC:29;
set SC = AffineMap r,a,r,b;
A5: AffineMap r,a,r,b is one-to-one by A1, JGRAPH_2:54;
A6: dom (AffineMap r,a,r,b) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A7: dom ((AffineMap r,a,r,b) | Kb) = (dom (AffineMap r,a,r,b)) /\ Kb by RELAT_1:90
.= the carrier of ((TOP-REAL 2) | Kb) by A4, A6, XBOOLE_1:28 ;
A8: rng ((AffineMap r,a,r,b) | Kb) c= ((AffineMap r,a,r,b) | Kb) .: the carrier of ((TOP-REAL 2) | Kb)

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in rng ((AffineMap r,a,r,b) | Kb) or u in ((AffineMap r,a,r,b) | Kb) .: the carrier of ((TOP-REAL 2) | Kb) )
assume u in rng ((AffineMap r,a,r,b) | Kb) ; :: thesis: u in ((AffineMap r,a,r,b) | Kb) .: the carrier of ((TOP-REAL 2) | Kb)
then consider z being set such that
A9: ( z in dom ((AffineMap r,a,r,b) | Kb) & u = ((AffineMap r,a,r,b) | Kb) . z ) by FUNCT_1:def 5;
thus u in ((AffineMap r,a,r,b) | Kb) .: the carrier of ((TOP-REAL 2) | Kb) by A7, A9, FUNCT_1:def 12; :: thesis: verum

end;

((AffineMap r,a,r,b) | Kb) .: the carrier of ((TOP-REAL 2) | Kb) = (AffineMap r,a,r,b) .: Kb by A4, RELAT_1:162
.= Cb by A1, Th29
.= the carrier of ((TOP-REAL 2) | Cbb) by PRE_TOPC:29 ;
then reconsider f0 = (AffineMap r,a,r,b) | Kb as Function of ((TOP-REAL 2) | Kb),((TOP-REAL 2) | Cbb) by A7, A8, FUNCT_2:4;
rng ((AffineMap r,a,r,b) | Kb) c= the carrier of (TOP-REAL 2) ;
then reconsider f00 = f0 as Function of ((TOP-REAL 2) | Kb),(TOP-REAL 2) by A7, FUNCT_2:4;
A10: rng f0 = ((AffineMap r,a,r,b) | Kb) .: the carrier of ((TOP-REAL 2) | Kb) by FUNCT_2:45
.= (AffineMap r,a,r,b) .: Kb by A4, RELAT_1:162
.= Cb by A1, Th29 ;
A11: f0 is one-to-one by A5, FUNCT_1:84;
A12: f00 is continuous by TOPMETR:10;
Kb is compact by Th31, JGRAPH_3:36;
then (TOP-REAL 2) | Kb is compact ;
then ex f1 being Function of ((TOP-REAL 2) | Kb),((TOP-REAL 2) | Cbb) st
( f00 = f1 & f1 is being_homeomorphism ) by A10, A11, A12, JGRAPH_1:64;
hence Cb is being_simple_closed_curve by Th30, JGRAPH_3:36; :: thesis: verum