let a, b, r be Real; :: 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:52;
A4: |[r,0]| `2 = 0 by EUCLID:52;
|.(|[(r + a),b]| - |[a,b]|).| = |.(|[(r + a),(0 + b)]| - |[a,b]|).|
.= |.((|[r,0]| + |[a,b]|) - |[a,b]|).| by EUCLID:56
.= |.(|[r,0]| + (|[a,b]| - |[a,b]|)).| by RLVECT_1:def 3
.= |.(|[r,0]| + (0. (TOP-REAL 2))).| by RLVECT_1:5
.= |.|[r,0]|.| by RLVECT_1:4
.= sqrt ((r ^2) + (0 ^2)) by A3, A4, JGRAPH_3:1
.= r by A1, SQUARE_1:22 ;
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:52;
|[1,0]| `2 = 0 by EUCLID:52;
then |.|[1,0]|.| = sqrt ((1 ^2) + (0 ^2)) by A5, JGRAPH_3:1
.= 1 ;
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:8;
set SC = AffineMap (r,a,r,b);
A8: AffineMap (r,a,r,b) is one-to-one by A1, JGRAPH_2:44;
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:61
.= 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 object ; :: 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 object st
( z in dom ((AffineMap (r,a,r,b)) | Kb) & u = ((AffineMap (r,a,r,b)) | Kb) . z ) by FUNCT_1:def 3;
hence u in ((AffineMap (r,a,r,b)) | Kb) .: the carrier of ((TOP-REAL 2) | Kb) by A10, FUNCT_1:def 6; :: 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:129
.= Cb by A1, A2, Th20
.= the carrier of ((TOP-REAL 2) | Cbb) by PRE_TOPC:8 ;
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:2;
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:2;
A12: rng f0 = ((AffineMap (r,a,r,b)) | Kb) .: the carrier of ((TOP-REAL 2) | Kb) by RELSET_1:22
.= (AffineMap (r,a,r,b)) .: Kb by A7, RELAT_1:129
.= Cb by A1, A2, Th20 ;
A13: f0 is one-to-one by A8, FUNCT_1:52;
Kb is compact by Th22, JGRAPH_3:26;
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:46, TOPMETR:7;
hence Cb is being_simple_closed_curve by Th21, JGRAPH_3:26; :: thesis: verum