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 that
A1: r > 0 and
A2: Cb = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } ; :: thesis: Cb is being_simple_closed_curve
A3: |[r,0 ]| `1 = r by EUCLID:56;
A4: |[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 A3, A4, JGRAPH_3:10
.= r by A1, SQUARE_1:89 ;
then |[(r + a),b]| in Cb by A2;
then reconsider Cbb = Cb as non empty Subset of (TOP-REAL 2) ;
set v = |[1,0 ]|;
A5: |[1,0 ]| `1 = 1 by EUCLID:56;
|[1,0 ]| `2 = 0 by EUCLID:56;
then |.|[1,0 ]|.| = sqrt ((1 ^2 ) + (0 ^2 )) by A5, JGRAPH_3:10
.= 1 by SQUARE_1:89 ;
then A6: |[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 A6;
A7: the carrier of ((TOP-REAL 2) | Kb) = Kb by PRE_TOPC:29;
set SC = AffineMap r,a,r,b;
A8: AffineMap r,a,r,b is one-to-one by A1, JGRAPH_2:54;
A9: dom (AffineMap r,a,r,b) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A10: 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 A7, A9, XBOOLE_1:28 ;
A11: 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 ex z being set st
( z in dom ((AffineMap r,a,r,b) | Kb) & u = ((AffineMap r,a,r,b) | Kb) . z ) by FUNCT_1:def 5;
hence u in ((AffineMap r,a,r,b) | Kb) .: the carrier of ((TOP-REAL 2) | Kb) by A10, 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 A7, RELAT_1:162
.= Cb by A1, A2, 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 A10, A11, 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 A10, FUNCT_2:4;
A12: 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 A7, RELAT_1:162
.= Cb by A1, A2, Th29 ;
A13: f0 is one-to-one by A8, FUNCT_1:84;
Kb is compact by Th31, JGRAPH_3:36;
then ex f1 being Function of ((TOP-REAL 2) | Kb),((TOP-REAL 2) | Cbb) st
( f00 = f1 & f1 is being_homeomorphism ) by A12, A13, JGRAPH_1:64, TOPMETR:10;
hence Cb is being_simple_closed_curve by Th30, JGRAPH_3:36; :: thesis: verum