jordan24.miz

begin

 reserve p1,p2 for Point of ( TOP-REAL 2),

C for Simple_closed_curve,

P for Subset of ( TOP-REAL 2);

 definition

 let n be Element of NAT , A be Subset of ( TOP-REAL n), a,b be Point of ( TOP-REAL n);

 :: JORDAN24:def1

 pred a,b realize-max-dist-in A means a in A & b in A & for x,y be Point of ( TOP-REAL n) st x in A & y in A holds ( dist (a,b)) >= ( dist (x,y));

 end

 set rl = ( - 1);

 set rp = 1;

 set a = |[rl, 0 ]|;

 set b = |[rp, 0 ]|;



 Lm1: the TopStruct of ( TOP-REAL 2) = ( TopSpaceMetr ( Euclid 2)) by EUCLID:def 8;

 theorem :: JORDAN24:1



 Th1: for C be non empty compact Subset of ( TOP-REAL 2) holds ex p1, p2 st (p1,p2) realize-max-dist-in C

 proof

 let C be non empty compact Subset of ( TOP-REAL 2);

 reconsider D = C as Subset of ( TopSpaceMetr ( Euclid 2)) by Lm1;



 A1: D is compact by Lm1, COMPTS_1: 23;

 then

 consider x1,x2 be Point of ( Euclid 2) such that

 A2: x1 in D & x2 in D and

 A3: ( dist (x1,x2)) = ( max_dist_max (D,D)) by WEIERSTR: 33;

 reconsider a = x1, b = x2 as Point of ( TOP-REAL 2) by EUCLID: 67;

 take a, b;

 thus a in C & b in C by A2;

 let x,y be Point of ( TOP-REAL 2) such that

 A4: x in C & y in C;

 reconsider x9 = x, y9 = y as Point of ( Euclid 2) by EUCLID: 67;

 ( dist (x9,y9)) <= ( max_dist_max (D,D)) by A1, A4, WEIERSTR: 34;

 then ( dist (x,y)) <= ( max_dist_max (D,D)) by TOPREAL6:def 1;

 hence thesis by A3, TOPREAL6:def 1;

 end;

 definition

 let M be non empty MetrStruct;

 let f be Function of ( TopSpaceMetr M), ( TopSpaceMetr M);

 :: JORDAN24:def2

 attr f is isometric means

 : Def2: ex g be isometric Function of M, M st g = f;

 end

 registration

 let M be non empty MetrStruct;

 cluster onto isometric for Function of ( TopSpaceMetr M), ( TopSpaceMetr M);

 existence

 proof

 set f = the onto isometric Function of M, M;

 reconsider f as Function of ( TopSpaceMetr M), ( TopSpaceMetr M);

 take f;

 thus thesis;

 end;

 end

 registration

 let M be non empty MetrSpace;

 cluster isometric -> continuous for Function of ( TopSpaceMetr M), ( TopSpaceMetr M);

 coherence

 proof

 let f be Function of ( TopSpaceMetr M), ( TopSpaceMetr M);

 assume f is isometric;

 then

 consider g be isometric Function of M, M such that

 A1: g = f;

 let W be Point of ( TopSpaceMetr M);

 let G be a_neighborhood of (f . W);

 reconsider fw = (f . W), w = W as Point of M;

 (f . W) in ( Int G) by CONNSP_2:def 1;

 then

 consider r be Real such that

 A2: r > 0 and

 A3: ( Ball (fw,r)) c= G by GOBOARD6: 4;

 reconsider H = ( Ball (w,r)) as a_neighborhood of W by A2, GOBOARD6: 91;

 take H;

 thus (f .: H) c= G

 proof

 let a be object;

 assume a in (f .: H);

 then

 consider b be object such that

 A4: b in ( dom f) and

 A5: b in H and

 A6: (f . b) = a by FUNCT_1:def 6;

 reconsider b as Point of ( TopSpaceMetr M) by A4;

 reconsider b9 = b as Point of M;

 ( dist (b9,w)) < r by A5, METRIC_1: 11;

 then ( dist ((g . b9),fw)) < r by A1, VECTMETR:def 3;

 then a in ( Ball (fw,r)) by A1, A6, METRIC_1: 11;

 hence thesis by A3;

 end;

 end;

 end

 registration

 let M be non empty MetrSpace;

 cluster onto isometric -> being_homeomorphism for Function of ( TopSpaceMetr M), ( TopSpaceMetr M);

 coherence

 proof

 let f be Function of ( TopSpaceMetr M), ( TopSpaceMetr M);

 assume

 A1: f is onto isometric;

 then

 reconsider f1 = f as onto isometric Function of ( TopSpaceMetr M), ( TopSpaceMetr M);

 thus ( dom f) = ( [#] ( TopSpaceMetr M)) by FUNCT_2:def 1;

 consider g be isometric Function of M, M such that

 A2: g = f by A1;

 g is onto by A1, A2;

 hence ( rng f) = ( [#] ( TopSpaceMetr M)) by A2;

 thus f is one-to-one by A2;

 f1 is continuous;

 hence f is continuous;

 (f " ) is isometric Function of ( TopSpaceMetr M), ( TopSpaceMetr M) by A1, Def2;

 hence thesis;

 end;

 end

 definition

 let a be Real;

 :: JORDAN24:def3

 func Rotate (a) -> Function of ( TOP-REAL 2), ( TOP-REAL 2) means

 : Def3: for p be Point of ( TOP-REAL 2) holds (it . p) = |[( Re ( Rotate (((p `1 ) + ((p `2 ) * )),a))), ( Im ( Rotate (((p `1 ) + ((p `2 ) * )),a)))]|;

 existence

 proof

 deffunc F( Point of ( TOP-REAL 2)) = |[( Re ( Rotate ((($1 `1 ) + (($1 `2 ) * )),a))), ( Im ( Rotate ((($1 `1 ) + (($1 `2 ) * )),a)))]|;

 consider f be Function of ( TOP-REAL 2), ( TOP-REAL 2) such that

 A1: for p be Point of ( TOP-REAL 2) holds (f . p) = F(p) from FUNCT_2:sch 4;

 take f;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let f,g be Function of ( TOP-REAL 2), ( TOP-REAL 2) such that

 A2: for p be Point of ( TOP-REAL 2) holds (f . p) = |[( Re ( Rotate (((p `1 ) + ((p `2 ) * )),a))), ( Im ( Rotate (((p `1 ) + ((p `2 ) * )),a)))]| and

 A3: for p be Point of ( TOP-REAL 2) holds (g . p) = |[( Re ( Rotate (((p `1 ) + ((p `2 ) * )),a))), ( Im ( Rotate (((p `1 ) + ((p `2 ) * )),a)))]|;

 now

 let p be Point of ( TOP-REAL 2);



 thus (f . p) = |[( Re ( Rotate (((p `1 ) + ((p `2 ) * )),a))), ( Im ( Rotate (((p `1 ) + ((p `2 ) * )),a)))]| by A2

 .= (g . p) by A3;

 end;

 hence f = g;

 end;

 end

 Lm2:

 now

 let a be Real;

 let c be Complex;

 let i be Integer;

 ( cos (a + ( Arg c))) = ( cos ((a + ( Arg c)) + ((2 * PI ) * i))) by COMPLEX2: 9;

 hence ( Rotate (c,a)) = ( Rotate (c,(a + ((2 * PI ) * i)))) by COMPLEX2: 8;

 end;

 Lm3:

 now

 let a be Real;

 let i be Integer;

 thus ( Rotate a) = ( Rotate (a + ((2 * PI ) * i)))

 proof

 let p be Point of ( TOP-REAL 2);

 set q = ((p `1 ) + ((p `2 ) * ));



 A1: ( Rotate (q,a)) = ( Rotate (q,(a + ((2 * PI ) * i)))) by Lm2;



 thus (( Rotate a) . p) = |[( Re ( Rotate (q,a))), ( Im ( Rotate (q,a)))]| by Def3

 .= (( Rotate (a + ((2 * PI ) * i))) . p) by A1, Def3;

 end;

 end;

 theorem :: JORDAN24:2



 Th2: for a be Real holds for f be Function of ( TopSpaceMetr ( Euclid 2)), ( TopSpaceMetr ( Euclid 2)) st f = ( Rotate a) holds f is onto isometric

 proof

 let a be Real;

 consider A be Real such that

 A1: A = (((2 * PI ) * ( - [\(a / (2 * PI ))/])) + a) and

 A2: 0 <= A and

 A3: A < (2 * PI ) by COMPLEX2: 1;

 reconsider A as Real;

 let f be Function of ( TopSpaceMetr ( Euclid 2)), ( TopSpaceMetr ( Euclid 2)) such that

 A4: f = ( Rotate a);

 reconsider g = f as Function of ( Euclid 2), ( Euclid 2);



 A5: ( Rotate A) = ( Rotate a) by A1, Lm3;

 g is onto isometric

 proof

 thus ( rng g) = the carrier of ( Euclid 2)

 proof

 thus ( rng g) c= the carrier of ( Euclid 2);

 let o be object;

 assume o in the carrier of ( Euclid 2);

 then

 reconsider p = o as Point of ( TOP-REAL 2) by EUCLID: 67;

 set pz = ((p `1 ) + ((p `2 ) * ));

 reconsider pz as Element of COMPLEX by XCMPLX_0:def 2;

 set arg = ( Arg pz);

 per cases ;

 suppose

 A6: pz <> 0 ;

 per cases ;

 suppose A <= arg;

 then

 A7: 0 <= (arg - A) by XREAL_1: 48;

 set qz = ( Rotate (pz,( - A)));



 A8: |.( Rotate (pz,( - A))).| = |.pz.| by COMPLEX2: 53;

 (arg - A) <= arg & arg < (2 * PI ) by A2, COMPTRIG: 34, XREAL_1: 43;

 then

 A9: (( - A) + arg) < (2 * PI ) by XXREAL_0: 2;

 qz <> 0 by A6, COMPLEX2: 52;

 then ( Arg qz) = (( - A) + arg) by A7, A9, A8, COMPTRIG:def 1;

 then

 A10: ( Rotate (qz,A)) = pz by A8, COMPTRIG: 62;

 set q = |[( Re qz), ( Im qz)]|;



 A11: ( dom g) = the carrier of ( Euclid 2) by FUNCT_2:def 1;

 (g . q) = |[( Re ( Rotate (((q `1 ) + ((q `2 ) * )),A))), ( Im ( Rotate (((q `1 ) + ((q `2 ) * )),A)))]| by A4, A5, Def3

 .= |[( Re ( Rotate ((( Re qz) + ((q `2 ) * )),A))), ( Im ( Rotate (((q `1 ) + ((q `2 ) * )),A)))]| by EUCLID: 52

 .= |[( Re ( Rotate ((( Re qz) + (( Im qz) * )),A))), ( Im ( Rotate (((q `1 ) + ((q `2 ) * )),A)))]| by EUCLID: 52

 .= |[( Re ( Rotate ((( Re qz) + (( Im qz) * )),A))), ( Im ( Rotate ((( Re qz) + ((q `2 ) * )),A)))]| by EUCLID: 52

 .= |[( Re ( Rotate ((( Re qz) + (( Im qz) * )),A))), ( Im ( Rotate ((( Re qz) + (( Im qz) * )),A)))]| by EUCLID: 52

 .= |[( Re ( Rotate (qz,A))), ( Im ( Rotate ((( Re qz) + (( Im qz) * )),A)))]| by COMPLEX1: 13

 .= |[( Re pz), ( Im pz)]| by A10, COMPLEX1: 13

 .= |[(p `1 ), ( Im pz)]| by COMPLEX1: 12

 .= |[(p `1 ), (p `2 )]| by COMPLEX1: 12

 .= p by EUCLID: 53;

 hence thesis by A11, Lm1, FUNCT_1:def 3;

 end;

 suppose A > arg;

 then (arg - A) < 0 by XREAL_1: 49;

 then

 A12: ((2 * PI ) + (arg - A)) < (2 * PI ) by XREAL_1: 30;

 set qz = ( Rotate (pz,( - A)));

 set q = |[( Re qz), ( Im qz)]|;



 A13: ( dom g) = the carrier of ( Euclid 2) by FUNCT_2:def 1;



 A14: |.( Rotate (pz,( - A))).| = |.pz.| by COMPLEX2: 53;

 then qz = (( |.qz.| * ( cos (((2 * PI ) * 1) + (( - A) + arg)))) + (( |.qz.| * ( sin (( - A) + arg))) * )) by COMPLEX2: 9;

 then

 A15: qz = (( |.qz.| * ( cos ((2 * PI ) + (arg - A)))) + (( |.qz.| * ( sin (((2 * PI ) * 1) + (( - A) + arg)))) * )) by COMPLEX2: 8;

 0 <= ((2 * PI ) - A) & arg >= 0 by A3, COMPTRIG: 34, XREAL_1: 48;

 then

 A16: 0 <= (((2 * PI ) - A) + arg);

 qz <> 0 by A6, COMPLEX2: 52;

 then ( Arg qz) = ((2 * PI ) + (arg - A)) by A16, A12, A15, COMPTRIG:def 1;

 then ( Rotate (qz,A)) = (( |.qz.| * ( cos arg)) + (( |.qz.| * ( sin (((2 * PI ) * 1) + arg))) * )) by COMPLEX2: 9;

 then ( Rotate (qz,A)) = (( |.qz.| * ( cos arg)) + (( |.qz.| * ( sin arg)) * )) by COMPLEX2: 8;

 then

 A17: ( Rotate (qz,A)) = pz by A14, COMPTRIG: 62;

 (g . q) = |[( Re ( Rotate (((q `1 ) + ((q `2 ) * )),A))), ( Im ( Rotate (((q `1 ) + ((q `2 ) * )),A)))]| by A4, A5, Def3

 .= |[( Re ( Rotate ((( Re qz) + ((q `2 ) * )),A))), ( Im ( Rotate (((q `1 ) + ((q `2 ) * )),A)))]| by EUCLID: 52

 .= |[( Re ( Rotate ((( Re qz) + (( Im qz) * )),A))), ( Im ( Rotate (((q `1 ) + ((q `2 ) * )),A)))]| by EUCLID: 52

 .= |[( Re ( Rotate ((( Re qz) + (( Im qz) * )),A))), ( Im ( Rotate ((( Re qz) + ((q `2 ) * )),A)))]| by EUCLID: 52

 .= |[( Re ( Rotate ((( Re qz) + (( Im qz) * )),A))), ( Im ( Rotate ((( Re qz) + (( Im qz) * )),A)))]| by EUCLID: 52

 .= |[( Re ( Rotate (qz,A))), ( Im ( Rotate ((( Re qz) + (( Im qz) * )),A)))]| by COMPLEX1: 13

 .= |[( Re pz), ( Im pz)]| by A17, COMPLEX1: 13

 .= |[(p `1 ), ( Im pz)]| by COMPLEX1: 12

 .= |[(p `1 ), (p `2 )]| by COMPLEX1: 12

 .= p by EUCLID: 53;

 hence thesis by A13, Lm1, FUNCT_1:def 3;

 end;

 end;

 suppose

 A18: pz = 0 ;

 reconsider z = 0 as Element of COMPLEX by XCMPLX_0:def 2;

 set q = |[ 0 , 0 ]|;



 A19: ( dom g) = the carrier of ( Euclid 2) by FUNCT_2:def 1;



 A20: (p `1 ) = 0 by A18, COMPLEX1: 4, COMPLEX1: 12;

 (g . q) = |[( Re ( Rotate (((q `1 ) + ((q `2 ) * )),a))), ( Im ( Rotate (((q `1 ) + ((q `2 ) * )),a)))]| by A4, Def3

 .= |[( Re ( Rotate ((z + ((q `2 ) * )),a))), ( Im ( Rotate (((q `1 ) + ((q `2 ) * )),a)))]| by EUCLID: 52

 .= |[( Re ( Rotate ((z + (z * )),a))), ( Im ( Rotate (((q `1 ) + ((q `2 ) * )),a)))]| by EUCLID: 52

 .= |[( Re ( Rotate ((z + (z * )),a))), ( Im ( Rotate ((z + ((q `2 ) * )),a)))]| by EUCLID: 52

 .= |[( Re ( Rotate (z,a))), ( Im ( Rotate (z,a)))]| by EUCLID: 52

 .= |[( Re z), ( Im ( Rotate (z,a)))]| by COMPLEX2: 52

 .= |[( Re z), ( Im z)]| by COMPLEX2: 52

 .= p by A18, A20, COMPLEX1: 4, EUCLID: 53;

 hence thesis by A19, Lm1, FUNCT_1:def 3;

 end;

 end;

 let X,Y be Point of ( Euclid 2);

 reconsider x = X, y = Y, gx = (g . X), gy = (g . Y) as Point of ( TOP-REAL 2) by EUCLID: 67;



 A21: ( |[( Re ( Rotate (((x `1 ) + ((x `2 ) * )),a))), ( Im ( Rotate (((x `1 ) + ((x `2 ) * )),a)))]| `1 ) = ( Re ( Rotate (((x `1 ) + ((x `2 ) * )),a))) & ( |[( Re ( Rotate (((x `1 ) + ((x `2 ) * )),a))), ( Im ( Rotate (((x `1 ) + ((x `2 ) * )),a)))]| `2 ) = ( Im ( Rotate (((x `1 ) + ((x `2 ) * )),a))) by EUCLID: 52;

 reconsider xx = ((x `1 ) + ((x `2 ) * )), yy = ((y `1 ) + ((y `2 ) * )) as Element of COMPLEX by XCMPLX_0:def 2;



 A22: ( |[( Re ( Rotate (((y `1 ) + ((y `2 ) * )),a))), ( Im ( Rotate (((y `1 ) + ((y `2 ) * )),a)))]| `1 ) = ( Re ( Rotate (((y `1 ) + ((y `2 ) * )),a))) & ( |[( Re ( Rotate (((y `1 ) + ((y `2 ) * )),a))), ( Im ( Rotate (((y `1 ) + ((y `2 ) * )),a)))]| `2 ) = ( Im ( Rotate (((y `1 ) + ((y `2 ) * )),a))) by EUCLID: 52;



 A23: ( Re ((y `1 ) + ((y `2 ) * ))) = (y `1 ) & ( Im ((y `1 ) + ((y `2 ) * ))) = (y `2 ) by COMPLEX1: 12;



 A24: ((( sin a) ^2 ) + (( cos a) ^2 )) = 1 by SIN_COS: 29;



 A25: ( Re ((x `1 ) + ((x `2 ) * ))) = (x `1 ) & ( Im ((x `1 ) + ((x `2 ) * ))) = (x `2 ) by COMPLEX1: 12;

 x = |[(x `1 ), (x `2 )]| & y = |[(y `1 ), (y `2 )]| by EUCLID: 53;



 hence ( dist (X,Y)) = ( sqrt ((((x `1 ) - (y `1 )) ^2 ) + (((x `2 ) - (y `2 )) ^2 ))) by GOBOARD6: 6

 .= ( sqrt ((((((x `1 ) * (x `1 )) - ((2 * (x `1 )) * (y `1 ))) + ((y `1 ) * (y `1 ))) * ((( sin a) * ( sin a)) + (( cos a) * ( cos a)))) + (((((x `2 ) * (x `2 )) - ((2 * (x `2 )) * (y `2 ))) + ((y `2 ) * (y `2 ))) * ((( sin a) ^2 ) + (( cos a) ^2 ))))) by A24

 .= ( sqrt ((((((x `1 ) * ( cos a)) - ((x `2 ) * ( sin a))) - (((y `1 ) * ( cos a)) - ((y `2 ) * ( sin a)))) ^2 ) + ((((((x `1 ) * ( sin a)) + ((x `2 ) * ( cos a))) ^2 ) - ((2 * (((x `1 ) * ( sin a)) + ((x `2 ) * ( cos a)))) * (((y `1 ) * ( sin a)) + ((y `2 ) * ( cos a))))) + ((((y `1 ) * ( sin a)) + ((y `2 ) * ( cos a))) ^2 ))))

 .= ( sqrt (((( Re ( Rotate (xx,a))) - (((y `1 ) * ( cos a)) - ((y `2 ) * ( sin a)))) ^2 ) + (((((x `1 ) * ( sin a)) + ((x `2 ) * ( cos a))) - (((y `1 ) * ( sin a)) + ((y `2 ) * ( cos a)))) ^2 ))) by A25, COMPLEX2: 56

 .= ( sqrt (((( Re ( Rotate (xx,a))) - (((y `1 ) * ( cos a)) - ((y `2 ) * ( sin a)))) ^2 ) + ((( Im ( Rotate (xx,a))) - (((y `1 ) * ( sin a)) + ((y `2 ) * ( cos a)))) ^2 ))) by A25, COMPLEX2: 56

 .= ( sqrt (((( Re ( Rotate (xx,a))) - ( Re ( Rotate (yy,a)))) ^2 ) + ((( Im ( Rotate (xx,a))) - (((y `1 ) * ( sin a)) + ((y `2 ) * ( cos a)))) ^2 ))) by A23, COMPLEX2: 56

 .= ( sqrt (((( Re ( Rotate (xx,a))) - ( Re ( Rotate (yy,a)))) ^2 ) + ((( Im ( Rotate (xx,a))) - ( Im ( Rotate (yy,a)))) ^2 ))) by A23, COMPLEX2: 56

 .= ( dist ( |[( Re ( Rotate (((x `1 ) + ((x `2 ) * )),a))), ( Im ( Rotate (((x `1 ) + ((x `2 ) * )),a)))]|, |[( Re ( Rotate (((y `1 ) + ((y `2 ) * )),a))), ( Im ( Rotate (((y `1 ) + ((y `2 ) * )),a)))]|)) by A21, A22, TOPREAL6: 92

 .= ( dist ( |[( Re ( Rotate (((x `1 ) + ((x `2 ) * )),a))), ( Im ( Rotate (((x `1 ) + ((x `2 ) * )),a)))]|,gy)) by A4, Def3

 .= ( dist (gx,gy)) by A4, Def3

 .= ( dist ((g . X),(g . Y))) by TOPREAL6:def 1;

 end;

 hence thesis;

 end;

 theorem :: JORDAN24:3



 Th3: for A,B,D be Real st (p1,p2) realize-max-dist-in P holds ((( AffineMap (A,B,A,D)) . p1),(( AffineMap (A,B,A,D)) . p2)) realize-max-dist-in (( AffineMap (A,B,A,D)) .: P)

 proof

 let A,B,D be Real;

 set a = p1, b = p2, C = P;



 A1: ( dom ( AffineMap (A,B,A,D))) = the carrier of ( TOP-REAL 2) by FUNCT_2:def 1;

 assume

 A2: (a,b) realize-max-dist-in C;

 then a in C;

 hence (( AffineMap (A,B,A,D)) . a) in (( AffineMap (A,B,A,D)) .: C) by A1, FUNCT_1:def 6;

 b in C by A2;

 hence (( AffineMap (A,B,A,D)) . b) in (( AffineMap (A,B,A,D)) .: C) by A1, FUNCT_1:def 6;

 let x,y be Point of ( TOP-REAL 2);

 assume x in (( AffineMap (A,B,A,D)) .: C);

 then

 consider X be object such that

 A3: X in ( dom ( AffineMap (A,B,A,D))) and

 A4: X in C and

 A5: (( AffineMap (A,B,A,D)) . X) = x by FUNCT_1:def 6;

 reconsider X as Point of ( TOP-REAL 2) by A3;

 assume y in (( AffineMap (A,B,A,D)) .: C);

 then

 consider Y be object such that

 A6: Y in ( dom ( AffineMap (A,B,A,D))) and

 A7: Y in C and

 A8: (( AffineMap (A,B,A,D)) . Y) = y by FUNCT_1:def 6;

 reconsider Y as Point of ( TOP-REAL 2) by A6;



 A9: (((X `1 ) - (Y `1 )) ^2 ) >= 0 & (((X `2 ) - (Y `2 )) ^2 ) >= 0 by XREAL_1: 63;



 A10: (((a `1 ) - (b `1 )) ^2 ) >= 0 & (((a `2 ) - (b `2 )) ^2 ) >= 0 by XREAL_1: 63;



 A11: (A ^2 ) >= 0 by XREAL_1: 63;

 then

 A12: ( sqrt (A ^2 )) >= 0 by SQUARE_1:def 2;



 A13: ( dist ((( AffineMap (A,B,A,D)) . a),(( AffineMap (A,B,A,D)) . b))) = ( dist ( |[((A * (a `1 )) + B), ((A * (a `2 )) + D)]|,(( AffineMap (A,B,A,D)) . b))) by JGRAPH_2:def 2

 .= ( dist ( |[((A * (a `1 )) + B), ((A * (a `2 )) + D)]|, |[((A * (b `1 )) + B), ((A * (b `2 )) + D)]|)) by JGRAPH_2:def 2

 .= ( sqrt (((( |[((A * (a `1 )) + B), ((A * (a `2 )) + D)]| `1 ) - ( |[((A * (b `1 )) + B), ((A * (b `2 )) + D)]| `1 )) ^2 ) + ((( |[((A * (a `1 )) + B), ((A * (a `2 )) + D)]| `2 ) - ( |[((A * (b `1 )) + B), ((A * (b `2 )) + D)]| `2 )) ^2 ))) by TOPREAL6: 92

 .= ( sqrt (((((A * (a `1 )) + B) - ( |[((A * (b `1 )) + B), ((A * (b `2 )) + D)]| `1 )) ^2 ) + ((( |[((A * (a `1 )) + B), ((A * (a `2 )) + D)]| `2 ) - ( |[((A * (b `1 )) + B), ((A * (b `2 )) + D)]| `2 )) ^2 ))) by EUCLID: 52

 .= ( sqrt (((((A * (a `1 )) + B) - ((A * (b `1 )) + B)) ^2 ) + ((( |[((A * (a `1 )) + B), ((A * (a `2 )) + D)]| `2 ) - ( |[((A * (b `1 )) + B), ((A * (b `2 )) + D)]| `2 )) ^2 ))) by EUCLID: 52

 .= ( sqrt (((((A * (a `1 )) + B) - ((A * (b `1 )) + B)) ^2 ) + ((((A * (a `2 )) + D) - ( |[((A * (b `1 )) + B), ((A * (b `2 )) + D)]| `2 )) ^2 ))) by EUCLID: 52

 .= ( sqrt (((((A * (a `1 )) + B) - ((A * (b `1 )) + B)) ^2 ) + ((((A * (a `2 )) + D) - ((A * (b `2 )) + D)) ^2 ))) by EUCLID: 52

 .= ( sqrt ((A ^2 ) * ((((a `1 ) - (b `1 )) ^2 ) + (((a `2 ) - (b `2 )) ^2 ))))

 .= (( sqrt (A ^2 )) * ( sqrt ((((a `1 ) - (b `1 )) ^2 ) + (((a `2 ) - (b `2 )) ^2 )))) by A11, A10, SQUARE_1: 29

 .= (( sqrt (A ^2 )) * ( dist (a,b))) by TOPREAL6: 92;



 A14: ( dist (x,y)) = ( dist ( |[((A * (X `1 )) + B), ((A * (X `2 )) + D)]|,(( AffineMap (A,B,A,D)) . Y))) by A5, A8, JGRAPH_2:def 2

 .= ( dist ( |[((A * (X `1 )) + B), ((A * (X `2 )) + D)]|, |[((A * (Y `1 )) + B), ((A * (Y `2 )) + D)]|)) by JGRAPH_2:def 2

 .= ( sqrt (((( |[((A * (X `1 )) + B), ((A * (X `2 )) + D)]| `1 ) - ( |[((A * (Y `1 )) + B), ((A * (Y `2 )) + D)]| `1 )) ^2 ) + ((( |[((A * (X `1 )) + B), ((A * (X `2 )) + D)]| `2 ) - ( |[((A * (Y `1 )) + B), ((A * (Y `2 )) + D)]| `2 )) ^2 ))) by TOPREAL6: 92

 .= ( sqrt (((((A * (X `1 )) + B) - ( |[((A * (Y `1 )) + B), ((A * (Y `2 )) + D)]| `1 )) ^2 ) + ((( |[((A * (X `1 )) + B), ((A * (X `2 )) + D)]| `2 ) - ( |[((A * (Y `1 )) + B), ((A * (Y `2 )) + D)]| `2 )) ^2 ))) by EUCLID: 52

 .= ( sqrt (((((A * (X `1 )) + B) - ((A * (Y `1 )) + B)) ^2 ) + ((( |[((A * (X `1 )) + B), ((A * (X `2 )) + D)]| `2 ) - ( |[((A * (Y `1 )) + B), ((A * (Y `2 )) + D)]| `2 )) ^2 ))) by EUCLID: 52

 .= ( sqrt (((((A * (X `1 )) + B) - ((A * (Y `1 )) + B)) ^2 ) + ((((A * (X `2 )) + D) - ( |[((A * (Y `1 )) + B), ((A * (Y `2 )) + D)]| `2 )) ^2 ))) by EUCLID: 52

 .= ( sqrt (((((A * (X `1 )) + B) - ((A * (Y `1 )) + B)) ^2 ) + ((((A * (X `2 )) + D) - ((A * (Y `2 )) + D)) ^2 ))) by EUCLID: 52

 .= ( sqrt ((A ^2 ) * ((((X `1 ) - (Y `1 )) ^2 ) + (((X `2 ) - (Y `2 )) ^2 ))))

 .= (( sqrt (A ^2 )) * ( sqrt ((((X `1 ) - (Y `1 )) ^2 ) + (((X `2 ) - (Y `2 )) ^2 )))) by A11, A9, SQUARE_1: 29

 .= (( sqrt (A ^2 )) * ( dist (X,Y))) by TOPREAL6: 92;

 ( dist (a,b)) >= ( dist (X,Y)) by A2, A4, A7;

 hence thesis by A13, A14, A12, XREAL_1: 64;

 end;

 theorem :: JORDAN24:4



 Th4: for A be Real st (p1,p2) realize-max-dist-in P holds ((( Rotate A) . p1),(( Rotate A) . p2)) realize-max-dist-in (( Rotate A) .: P)

 proof

 let A be Real;

 reconsider f = ( Rotate A) as Function of ( TopSpaceMetr ( Euclid 2)), ( TopSpaceMetr ( Euclid 2)) by Lm1;

 set C = P;



 A1: ( dom ( Rotate A)) = the carrier of ( TOP-REAL 2) by FUNCT_2:def 1;

 assume

 A2: (p1,p2) realize-max-dist-in C;

 then p1 in C & p2 in C;

 hence (( Rotate A) . p1) in (( Rotate A) .: C) & (( Rotate A) . p2) in (( Rotate A) .: C) by A1, FUNCT_1:def 6;

 let x,y be Point of ( TOP-REAL 2) such that

 A3: x in (( Rotate A) .: C) and

 A4: y in (( Rotate A) .: C);

 f is isometric by Th2;

 then

 consider g be isometric Function of ( Euclid 2), ( Euclid 2) such that

 A5: f = g;

 consider yy be object such that

 A6: yy in ( dom ( Rotate A)) and

 A7: yy in C and

 A8: (( Rotate A) . yy) = y by A4, FUNCT_1:def 6;

 reconsider yy as Point of ( TOP-REAL 2) by A6;

 consider xx be object such that

 A9: xx in ( dom ( Rotate A)) and

 A10: xx in C and

 A11: (( Rotate A) . xx) = x by A3, FUNCT_1:def 6;

 reconsider xx as Point of ( TOP-REAL 2) by A9;

 reconsider p19 = p1, p29 = p2, xx9 = xx, yy9 = yy as Point of ( Euclid 2) by EUCLID: 67;

 ( dist (p1,p2)) >= ( dist (xx,yy)) by A2, A10, A7;

 then ( dist (p19,p29)) >= ( dist (xx,yy)) by TOPREAL6:def 1;

 then ( dist (p19,p29)) >= ( dist (xx9,yy9)) by TOPREAL6:def 1;

 then ( dist ((g . p19),(g . p29))) >= ( dist (xx9,yy9)) by VECTMETR:def 3;

 then ( dist ((g . p19),(g . p29))) >= ( dist ((g . xx9),(g . yy9))) by VECTMETR:def 3;

 then ( dist ((( Rotate A) . p1),(( Rotate A) . p2))) >= ( dist ((g . xx9),(g . yy9))) by A5, TOPREAL6:def 1;

 hence thesis by A11, A8, A5, TOPREAL6:def 1;

 end;

 theorem :: JORDAN24:5



 Th5: for z be Complex, r be Real holds ( Rotate (z,( - r))) = ( Rotate (z,((2 * PI ) - r)))

 proof

 let z be Complex, r be Real;



 thus ( Rotate (z,( - r))) = (( |.z.| * ( cos (((2 * PI ) * 1) + (( - r) + ( Arg z))))) + (( |.z.| * ( sin (( - r) + ( Arg z)))) * )) by COMPLEX2: 9

 .= ( Rotate (z,((2 * PI ) - r))) by COMPLEX2: 8;

 end;

 theorem :: JORDAN24:6



 Th6: for r be Real holds ( Rotate ( - r)) = ( Rotate ((2 * PI ) - r))

 proof

 let r be Real;

 now

 let p be Point of ( TOP-REAL 2);



 thus (( Rotate ((2 * PI ) - r)) . p) = |[( Re ( Rotate (((p `1 ) + ((p `2 ) * )),((2 * PI ) - r)))), ( Im ( Rotate (((p `1 ) + ((p `2 ) * )),((2 * PI ) - r))))]| by Def3

 .= |[( Re ( Rotate (((p `1 ) + ((p `2 ) * )),( - r)))), ( Im ( Rotate (((p `1 ) + ((p `2 ) * )),((2 * PI ) - r))))]| by Th5

 .= |[( Re ( Rotate (((p `1 ) + ((p `2 ) * )),( - r)))), ( Im ( Rotate (((p `1 ) + ((p `2 ) * )),( - r))))]| by Th5;

 end;

 hence thesis by Def3;

 end;



 Lm4: for T1,T2 be TopSpace, f be Function of T1, T2, g be Function of the TopStruct of T1, the TopStruct of T2 st g = f & g is being_homeomorphism holds f is being_homeomorphism by PRE_TOPC: 34;

 theorem :: JORDAN24:7

 ex f be Homeomorphism of ( TOP-REAL 2) st ( |[( - 1), 0 ]|, |[1, 0 ]|) realize-max-dist-in (f .: C)

 proof

 reconsider z = 0 as Element of COMPLEX by XCMPLX_0:def 2;

 consider x,y be Point of ( TOP-REAL 2) such that

 A1: x <> y and

 A2: x in C & y in C by TOPREAL2: 4;



 A3: ( dist (x,y)) > 0 by A1, JORDAN1K: 22;

 consider p1, p2 such that

 A4: (p1,p2) realize-max-dist-in C by Th1;

 reconsider g = ( AffineMap (1,( - (p1 `1 )),1,( - (p1 `2 )))) as being_homeomorphism Function of ( TOP-REAL 2), ( TOP-REAL 2) by JGRAPH_7: 50;

 set D = (g .: C), q1 = (g . p1), q2 = (g . p2);

 set arg = ( Arg ((q2 `1 ) + ((q2 `2 ) * )));

 reconsider qq = ((q2 `1 ) + ((q2 `2 ) * )) as Element of COMPLEX by XCMPLX_0:def 2;

 set h = ( Rotate ( - arg));



 A5: h = ( Rotate ((2 * PI ) - arg)) by Th6;

 (q1,q2) realize-max-dist-in D by A4, Th3;

 then

 A6: ((( Rotate ((2 * PI ) - arg)) . q1),(( Rotate ((2 * PI ) - arg)) . q2)) realize-max-dist-in (( Rotate ((2 * PI ) - arg)) .: D) by Th4;

 reconsider h0 = h as onto isometric Function of ( TopSpaceMetr ( Euclid 2)), ( TopSpaceMetr ( Euclid 2)) by Lm1, Th2;



 A7: ( Rotate (z,( - arg))) = 0 by COMPLEX2: 52;

 h0 is being_homeomorphism;

 then

 reconsider h as being_homeomorphism Function of ( TOP-REAL 2), ( TOP-REAL 2) by Lm1, Lm4;

 set F = (h .: D), s1 = (h . q1), s2 = (h . q2);

 q1 = |[((1 * (p1 `1 )) + ( - (p1 `1 ))), ((1 * (p1 `2 )) + ( - (p1 `2 )))]| by JGRAPH_2:def 2

 .= |[ 0 , 0 ]|;



 then

 A8: s1 = |[( Re ( Rotate ((( |[ 0 , 0 ]| `1 ) + (( |[ 0 , 0 ]| `2 ) * )),( - arg)))), ( Im ( Rotate ((( |[ 0 , 0 ]| `1 ) + (( |[ 0 , 0 ]| `2 ) * )),( - arg))))]| by Def3

 .= |[( Re ( Rotate (( 0 + (( |[ 0 , 0 ]| `2 ) * )),( - arg)))), ( Im ( Rotate ((( |[ 0 , 0 ]| `1 ) + (( |[ 0 , 0 ]| `2 ) * )),( - arg))))]| by EUCLID: 52

 .= |[( Re ( Rotate (( 0 + ( 0 * )),( - arg)))), ( Im ( Rotate ((( |[ 0 , 0 ]| `1 ) + (( |[ 0 , 0 ]| `2 ) * )),( - arg))))]| by EUCLID: 52

 .= |[( Re ( Rotate (( 0 + ( 0 * )),( - arg)))), ( Im ( Rotate (( 0 + (( |[ 0 , 0 ]| `2 ) * )),( - arg))))]| by EUCLID: 52

 .= |[ 0 , 0 ]| by A7, COMPLEX1: 4, EUCLID: 52;

 ( Rotate (qq,( - arg))) = ( |.((q2 `1 ) + ((q2 `2 ) * )).| + ( 0 * )) by COMPLEX2: 55;



 then

 A9: s2 = |[( Re ( |.((q2 `1 ) + ((q2 `2 ) * )).| + ( 0 * ))), ( Im ( |.((q2 `1 ) + ((q2 `2 ) * )).| + ( 0 * )))]| by Def3

 .= |[ |.((q2 `1 ) + ((q2 `2 ) * )).|, ( Im ( |.((q2 `1 ) + ((q2 `2 ) * )).| + ( 0 * )))]| by COMPLEX1: 12

 .= |[ |.((q2 `1 ) + ((q2 `2 ) * )).|, 0 ]| by COMPLEX1: 12;

 then

 A10: (s2 `2 ) = 0 by EUCLID: 52;

 ( dist (p1,p2)) >= ( dist (x,y)) by A4, A2;

 then

 A11: p1 <> p2 by A3, TOPREAL6: 93;

 A12:

 now

 ( dom g) = the carrier of ( TOP-REAL 2) by FUNCT_2:def 1;

 then

 A13: q1 <> q2 by A11, FUNCT_1:def 4;

 assume

 A14: (s2 `1 ) = 0 ;

 ( dom h) = the carrier of ( TOP-REAL 2) by FUNCT_2:def 1;

 then s1 <> s2 by A13, FUNCT_1:def 4;

 hence contradiction by A8, A9, A14, EUCLID: 52;

 end;

 (s2 `1 ) = |.((q2 `1 ) + ((q2 `2 ) * )).| by A9, EUCLID: 52;

 then (s2 `1 ) >= 0 by COMPLEX1: 46;

 then

 reconsider j = ( AffineMap ((2 / (s2 `1 )),( - 1),(2 / (s2 `1 )), 0 )) as being_homeomorphism Function of ( TOP-REAL 2), ( TOP-REAL 2) by A12, JGRAPH_7: 50;

 set E = (j .: F), r1 = (j . s1), r2 = (j . s2);



 A15: r2 = |[(((2 / (s2 `1 )) * (s2 `1 )) + ( - 1)), (((2 / (s2 `1 )) * (s2 `2 )) + 0 )]| by JGRAPH_2:def 2

 .= |[(2 + ( - 1)), (((2 / (s2 `1 )) * (s2 `2 )) + 0 )]| by A12, XCMPLX_1: 87

 .= b by A10;

 set f = (j * (h * g));

 (h * g) is being_homeomorphism by TOPS_2: 57;

 then f is being_homeomorphism by TOPS_2: 57;

 then

 reconsider f as Homeomorphism of ( TOP-REAL 2) by TOPGRP_1:def 4;

 take f;

 ((h * g) .: C) = F by RELAT_1: 126;

 then

 A16: (f .: C) = E by RELAT_1: 126;

 r1 = |[(((2 / (s2 `1 )) * (s1 `1 )) + ( - 1)), (((2 / (s2 `1 )) * (s1 `2 )) + 0 )]| by JGRAPH_2:def 2

 .= |[(((2 / (s2 `1 )) * 0 ) + ( - 1)), (((2 / (s2 `1 )) * (s1 `2 )) + 0 )]| by A8, EUCLID: 52

 .= a by A8, EUCLID: 52;

 hence thesis by A5, A15, A16, A6, Th3;

 end;

 definition

 let T1,T2 be TopStruct;

 let f be Function of T1, T2;

 :: JORDAN24:def4

 attr f is closed means for A be Subset of T1 st A is closed holds (f .: A) is closed;

 end

 theorem :: JORDAN24:8

 for X,Y be non empty TopSpace, f be continuous Function of X, Y st f is one-to-one onto holds f is being_homeomorphism iff f is closed

 proof

 let X,Y be non empty TopSpace;

 let f be continuous Function of X, Y such that

 A1: f is one-to-one onto;

 thus f is being_homeomorphism implies f is closed by TOPS_2: 58;

 assume

 A2: for A be Subset of X st A is closed holds (f .: A) is closed;



 A3: ( [#] X) = the carrier of X & ( [#] Y) = the carrier of Y;



 A4: ( dom f) = the carrier of X by FUNCT_2:def 1;

 A5:

 now

 let A be Subset of X;

 assume (f .: A) is closed;

 then (f " (f .: A)) is closed by PRE_TOPC:def 6;

 hence A is closed by A1, A4, FUNCT_1: 94;

 end;

 thus thesis by A1, A2, A4, A3, A5, TOPS_2: 58;

 end;

 theorem :: JORDAN24:9



 Th9: for X be set, A be Subset of X holds (A ` ) = {} iff A = X by XBOOLE_1: 37;

 theorem :: JORDAN24:10

 for T1,T2 be non empty TopSpace, f be Function of T1, T2 st f is being_homeomorphism holds for A be Subset of T1 st A is connected holds (f .: A) is connected by TOPS_2: 61;

 theorem :: JORDAN24:11



 Th11: for T1,T2 be non empty TopSpace, f be Function of T1, T2 st f is being_homeomorphism holds for A be Subset of T1 st A is a_component holds (f .: A) is a_component

 proof

 let T1,T2 be non empty TopSpace, f be Function of T1, T2;

 assume

 A1: f is being_homeomorphism;

 let A be Subset of T1;

 assume that

 A2: A is connected and

 A3: for B be Subset of T1 st B is connected holds A c= B implies A = B;

 thus (f .: A) is connected by A1, A2, TOPS_2: 61;

 let B be Subset of T2;

 ( rng f) = the carrier of T2 by A1;

 then

 A4: (f .: (f " B)) = B by FUNCT_1: 77;



 A5: (f " (f .: A)) = A by A1, FUNCT_1: 94;

 assume that

 A6: B is connected and

 A7: (f .: A) c= B;

 (f " B) is connected by A1, A6, TOPS_2: 62;

 hence thesis by A3, A4, A5, A7, RELAT_1: 143;

 end;

 theorem :: JORDAN24:12



 Th12: for T1,T2 be non empty TopSpace, f be Function of T1, T2, A be Subset of T1 holds (f | A) is Function of (T1 | A), (T2 | (f .: A))

 proof

 let T1,T2 be non empty TopSpace, f be Function of T1, T2, A be Subset of T1;



 A1: ( rng (f | A)) = (f .: A) by RELAT_1: 115;

 ( dom f) = the carrier of T1 by FUNCT_2:def 1;

 then

 A2: ( dom (f | A)) = A by RELAT_1: 62;

 ( [#] (T1 | A)) = A & ( [#] (T2 | (f .: A))) = (f .: A) by PRE_TOPC:def 5;

 hence thesis by A2, A1, FUNCT_2: 2;

 end;

 theorem :: JORDAN24:13



 Th13: for T1,T2 be non empty TopSpace, f be Function of T1, T2 st f is continuous holds for A be Subset of T1, g be Function of (T1 | A), (T2 | (f .: A)) st g = (f | A) holds g is continuous

 proof

 let T1,T2 be non empty TopSpace;

 let f be Function of T1, T2;

 assume

 A1: f is continuous;

 let A be Subset of T1;

 let g be Function of (T1 | A), (T2 | (f .: A));

 assume

 A2: g = (f | A);



 A3: ( dom f) = the carrier of T1 by FUNCT_2:def 1;



 A4: ( [#] (T1 | A)) = A by PRE_TOPC:def 5;

 per cases ;

 suppose A is empty;

 hence thesis by TIETZE: 4;

 end;

 suppose A is non empty;

 then

 reconsider S1 = (T1 | A), S2 = (T2 | (f .: A)) as non empty TopSpace by A3;

 (f | A) = (f | (T1 | A)) by A4, TMAP_1:def 3;

 then

 A5: g is continuous Function of S1, T2 by A1, A2;

 g is Function of S1, S2;

 hence thesis by A5, JORDAN16: 8;

 end;

 end;

 theorem :: JORDAN24:14



 Th14: for T1,T2 be non empty TopSpace, f be Function of T1, T2 st f is being_homeomorphism holds for A be Subset of T1, g be Function of (T1 | A), (T2 | (f .: A)) st g = (f | A) holds g is being_homeomorphism

 proof

 let T1,T2 be non empty TopSpace;

 let f be Function of T1, T2;

 assume that

 A1: ( dom f) = ( [#] T1) and

 A2: ( rng f) = ( [#] T2) and

 A3: f is one-to-one and

 A4: f is continuous and

 A5: (f " ) is continuous;

 let A be Subset of T1;

 f is onto by A2;

 then

 A6: (f qua Function " ) = (f " ) by A3, TOPS_2:def 4;



 then

 A7: ((f " ) .: (f .: A)) = (f " (f .: A)) by A3, FUNCT_1: 85

 .= A by A1, A3, FUNCT_1: 94;



 A8: ( dom f) = the carrier of T1 by FUNCT_2:def 1;

 let g be Function of (T1 | A), (T2 | (f .: A));

 assume

 A9: g = (f | A);

 ( [#] (T1 | A)) = A & ( [#] (T2 | (f .: A))) = (f .: A) by PRE_TOPC:def 5;

 hence

 A10: ( dom g) = ( [#] (T1 | A)) & ( rng g) = ( [#] (T2 | (f .: A))) by A9, A8, RELAT_1: 62, RELAT_1: 115;



 A11: g is onto by A10;

 thus g is one-to-one by A3, A9, FUNCT_1: 52;

 then

 A12: (g qua Function " ) = (g " ) by A11, TOPS_2:def 4;

 thus g is continuous by A4, A9, Th13;

 (g " ) = ((f " ) | (f .: A)) by A3, A9, A6, A12, RFUNCT_2: 17;

 hence thesis by A5, A7, Th13;

 end;

 theorem :: JORDAN24:15



 Th15: for T1,T2 be non empty TopSpace, f be Function of T1, T2 st f is being_homeomorphism holds for A,B be Subset of T1 st A is_a_component_of B holds (f .: A) is_a_component_of (f .: B)

 proof

 let T1,T2 be non empty TopSpace, f be Function of T1, T2 such that

 A1: f is being_homeomorphism;

 let A,B be Subset of T1;

 given A1 be Subset of (T1 | B) such that

 A2: A1 = A and

 A3: A1 is a_component;



 A4: ( [#] (T2 | (f .: B))) = (f .: B) by PRE_TOPC:def 5;



 A5: ( dom f) = the carrier of T1 by FUNCT_2:def 1;



 A6: ( [#] (T1 | B)) = B by PRE_TOPC:def 5;

 then

 reconsider A2 = (f .: A) as Subset of (T2 | (f .: B)) by A2, A4, RELAT_1: 123;

 per cases ;

 suppose

 A7: B is empty;

 then (f .: B) = {} ;

 then

 A8: A2 = {} by A4, XBOOLE_1: 3;

 ( {} T2) = (f .: B) by A7;

 hence thesis by A8, JORDAN1K: 6;

 end;

 suppose B is non empty;

 then

 reconsider S1 = (T1 | B), S2 = (T2 | (f .: B)) as non empty TopSpace by A5;

 take A2;

 thus A2 = (f .: A);

 reconsider fB = (f | B) as Function of S1, S2 by Th12;

 (fB .: A) = A2 by A2, A6, RELAT_1: 129;

 hence thesis by A1, A2, A3, Th11, Th14;

 end;

 end;

 theorem :: JORDAN24:16

 for S be Subset of ( TOP-REAL 2), f be Homeomorphism of ( TOP-REAL 2) st S is Jordan holds (f .: S) is Jordan

 proof

 let S be Subset of ( TOP-REAL 2), f be Homeomorphism of ( TOP-REAL 2);

 set s = the Element of (S ` );

 assume

 A1: (S ` ) <> {} ;

 then s in (S ` );

 then

 reconsider s as Element of ( TOP-REAL 2);

 given A1,A2 be Subset of ( TOP-REAL 2) such that

 A2: (S ` ) = (A1 \/ A2) and

 A3: A1 misses A2 and

 A4: (( Cl A1) \ A1) = (( Cl A2) \ A2) and

 A5: A1 is_a_component_of (S ` ) & A2 is_a_component_of (S ` );



 A6: not s in S by A1, XBOOLE_0:def 5;

 hereby

 assume ((f .: S) ` ) = {} ;

 then (f .: S) = the carrier of ( TOP-REAL 2) by Th9;

 then ex s9 be Element of ( TOP-REAL 2) st s9 in S & (f . s) = (f . s9) by FUNCT_2: 65;

 hence contradiction by A6, FUNCT_2: 56;

 end;

 take B1 = (f .: A1), B2 = (f .: A2);

 (f .: (A1 \/ A2)) = (B1 \/ B2) by RELAT_1: 120;

 hence ((f .: S) ` ) = (B1 \/ B2) by A2, JORDAN1K: 5;

 thus B1 misses B2 by A3, FUNCT_1: 66;



 thus (( Cl B1) \ B1) = ((f .: ( Cl A1)) \ B1) by TOPS_2: 60

 .= (f .: (( Cl A2) \ A2)) by A4, FUNCT_1: 64

 .= ((f .: ( Cl A2)) \ B2) by FUNCT_1: 64

 .= (( Cl B2) \ B2) by TOPS_2: 60;

 (f .: (S ` )) = ((f .: S) ` ) by JORDAN1K: 5;

 hence thesis by A5, Th15;

 end;