let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis:
let P be non empty compact Subset of (TOP-REAL 2); :: thesis:
assume that
A1: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } and
A2: LE p1,p2,P and
A3: LE p2,p3,P and
A4: LE p3,p4,P and
A5: p1 <> p2 and
A6: p2 <> p3 and
A7: p3 <> p4 and
A8: p1 `1 < 0 and
A9: p2 `1 < 0 and
A10: p3 `1 < 0 and
A11: p4 `1 < 0 and
A12: p1 `2 < 0 and
A13: p2 `2 < 0 and
A14: p3 `2 < 0 ; :: thesis:
set q2 = ((p1 `2) -FanMorphW) . p2;
set q3 = ((p1 `2) -FanMorphW) . p3;
A15: p1 `2 < p2 `2 by A1, A2, A5, A8, A12, Th45;
set q1 = ((p1 `2) -FanMorphW) . p1;
A16: P is being_simple_closed_curve by A1, JGRAPH_3:26;
then p1 in P by A2, JORDAN7:5;
then A17: ex p11 being Point of (TOP-REAL 2) st
( p11 = p1 & |.p11.| = 1 ) by A1;
then A18: (p1 `2) / |.p1.| = p1 `2 ;
then A19: (((p1 `2) -FanMorphW) . p1) `2 = 0 by A8, JGRAPH_4:47;
A20: |.(((p1 `2) -FanMorphW) . p1).| = 1 by A17, JGRAPH_4:33;
then A21: ((((p1 `2) -FanMorphW) . p1) `2) / |.(((p1 `2) -FanMorphW) . p1).| = (((p1 `2) -FanMorphW) . p1) `2 ;
p2 in P by A2, A16, JORDAN7:5;
then A22: ex p22 being Point of (TOP-REAL 2) st
( p22 = p2 & |.p22.| = 1 ) by A1;
then A23: (p2 `2) / |.p2.| = p2 `2 ;
then A24: (((p1 `2) -FanMorphW) . p2) `1 < 0 by A9, A12, A15, JGRAPH_4:42;
A25: |.(((p1 `2) -FanMorphW) . p2).| = 1 by A22, JGRAPH_4:33;
then A26: ((((p1 `2) -FanMorphW) . p2) `2) / |.(((p1 `2) -FanMorphW) . p2).| = (((p1 `2) -FanMorphW) . p2) `2 ;
then A27: (((p1 `2) -FanMorphW) . p1) `2 < (((p1 `2) -FanMorphW) . p2) `2 by A8, A9, A12, A15, A18, A23, A21, JGRAPH_4:44;
then A28: (((p1 `2) -FanMorphW) . p2) `1 < 1 by A25, A19, Th2;
p3 in P by A3, A16, JORDAN7:5;
then A29: ex p33 being Point of (TOP-REAL 2) st
( p33 = p3 & |.p33.| = 1 ) by A1;
then A30: |.(((p1 `2) -FanMorphW) . p3).| = 1 by JGRAPH_4:33;
then A31: ((((p1 `2) -FanMorphW) . p3) `2) / |.(((p1 `2) -FanMorphW) . p3).| = (((p1 `2) -FanMorphW) . p3) `2 ;
set r3 = (((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3);
set r2 = (((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2);
A32: ((((p1 `2) -FanMorphW) . p3) `1) / |.(((p1 `2) -FanMorphW) . p3).| = (((p1 `2) -FanMorphW) . p3) `1 by A30;
A33: p2 `2 < p3 `2 by A1, A3, A6, A9, A13, Th45;
then A34: (p3 `2) / |.p3.| > p1 `2 by A15, A29, XXREAL_0:2;
then A35: (((p1 `2) -FanMorphW) . p3) `1 < 0 by A10, A12, JGRAPH_4:42;
A36: 1 ^2 = (((((p1 `2) -FanMorphW) . p3) `1) ^2) + (((((p1 `2) -FanMorphW) . p3) `2) ^2) by A30, JGRAPH_3:1;
A37: 1 ^2 = (((((p1 `2) -FanMorphW) . p2) `1) ^2) + (((((p1 `2) -FanMorphW) . p2) `2) ^2) by A25, JGRAPH_3:1;
(p3 `2) / |.p3.| > p2 `2 by A1, A3, A6, A9, A13, A29, Th45;
then A38: (((p1 `2) -FanMorphW) . p2) `2 < (((p1 `2) -FanMorphW) . p3) `2 by A9, A10, A12, A15, A23, A26, A31, A34, JGRAPH_4:44;
then ((((p1 `2) -FanMorphW) . p3) `2) ^2 > ((((p1 `2) -FanMorphW) . p2) `2) ^2 by A19, A27, SQUARE_1:16;
then (- ((((p1 `2) -FanMorphW) . p2) `1)) ^2 > ((((p1 `2) -FanMorphW) . p3) `1) ^2 by A37, A36, XREAL_1:8;
then A39: - (- ((((p1 `2) -FanMorphW) . p2) `1)) < (((p1 `2) -FanMorphW) . p3) `1 by A24, SQUARE_1:48;
A40: 0 < (((p1 `2) -FanMorphW) . p3) `2 by A8, A10, A12, A18, A21, A31, A19, A34, JGRAPH_4:44;
then A41: ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2 > 0 by A39, A28, A32, JGRAPH_4:75;
A42: |.((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)).| = 1 by A30, JGRAPH_4:66;
then A43: (((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `1) / |.((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)).| = ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `1 ;
A44: - 1 < p1 `2 by A8, A12, A17, Th2;
then consider f1 being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A45: f1 = (p1 `2) -FanMorphW and
A46: f1 is being_homeomorphism by A12, JGRAPH_4:41;
A47: - 1 < (((p1 `2) -FanMorphW) . p2) `1 by A12, A44, A25, A19, A27, Th2;
then consider f2 being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A48: f2 = ((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN and
A49: f2 is being_homeomorphism by A28, JGRAPH_4:74;
A50: ((((p1 `2) -FanMorphW) . p2) `1) / |.(((p1 `2) -FanMorphW) . p2).| = (((p1 `2) -FanMorphW) . p2) `1 by A25;
then A51: ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2)) `1 = 0 by A19, A27, JGRAPH_4:80;
A52: |.((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2)).| = 1 by A25, JGRAPH_4:66;
then A53: (((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2)) `1) / |.((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2)).| = ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2)) `1 ;
then A54: ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2)) `1 < ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `1 by A19, A27, A38, A39, A47, A28, A50, A32, A43, JGRAPH_4:79;
then A55: - 1 < ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2 by A12, A44, A42, A51, Th2;
(((p1 `2) -FanMorphW) . p1) `2 < (((p1 `2) -FanMorphW) . p2) `2 by A8, A9, A12, A15, A18, A23, A21, A26, JGRAPH_4:44;
then A56: ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2)) `1 < ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `1 by A19, A40, A39, A47, A28, A50, A32, A53, A43, JGRAPH_4:79;
set q4 = ((p1 `2) -FanMorphW) . p4;
p4 in P by A4, A16, JORDAN7:5;
then A57: ex p44 being Point of (TOP-REAL 2) st
( p44 = p4 & |.p44.| = 1 ) by A1;
then A58: |.(((p1 `2) -FanMorphW) . p4).| = 1 by JGRAPH_4:33;
then A59: ((((p1 `2) -FanMorphW) . p4) `2) / |.(((p1 `2) -FanMorphW) . p4).| = (((p1 `2) -FanMorphW) . p4) `2 ;
p3 `2 < p4 `2 by A1, A4, A7, A10, A14, Th45;
then (p4 `2) / |.p4.| > p2 `2 by A33, A57, XXREAL_0:2;
then A60: (p4 `2) / |.p4.| > p1 `2 by A15, XXREAL_0:2;
(p4 `2) / |.p4.| > p3 `2 by A1, A4, A7, A10, A14, A57, Th45;
then (((p1 `2) -FanMorphW) . p3) `2 < (((p1 `2) -FanMorphW) . p4) `2 by A10, A11, A12, A29, A31, A59, A34, A60, JGRAPH_4:44;
then A61: ((((p1 `2) -FanMorphW) . p4) `2) ^2 > ((((p1 `2) -FanMorphW) . p3) `2) ^2 by A19, A27, A38, SQUARE_1:16;
1 ^2 = (((((p1 `2) -FanMorphW) . p4) `1) ^2) + (((((p1 `2) -FanMorphW) . p4) `2) ^2) by A58, JGRAPH_3:1;
then (- ((((p1 `2) -FanMorphW) . p3) `1)) ^2 > ((((p1 `2) -FanMorphW) . p4) `1) ^2 by A36, A61, XREAL_1:8;
then - (- ((((p1 `2) -FanMorphW) . p3) `1)) < (((p1 `2) -FanMorphW) . p4) `1 by A35, SQUARE_1:48;
then A62: ((((p1 `2) -FanMorphW) . p4) `1) / |.(((p1 `2) -FanMorphW) . p4).| > (((p1 `2) -FanMorphW) . p3) `1 by A58;
set r4 = (((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4);
A63: 1 ^2 = ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `1) ^2) + ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) ^2) by A42, JGRAPH_3:1;
A64: |.((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)).| = 1 by A58, JGRAPH_4:66;
then A65: (((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)) `1) / |.((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)).| = ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)) `1 ;
set r1 = (((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p1);
|.(((p1 `2) -FanMorphW) . p1).| ^2 = (((((p1 `2) -FanMorphW) . p1) `1) ^2) + (((((p1 `2) -FanMorphW) . p1) `2) ^2) by JGRAPH_3:1;
then A66: ( (((p1 `2) -FanMorphW) . p1) `1 = - 1 or (((p1 `2) -FanMorphW) . p1) `1 = 1 ) by A20, A19, SQUARE_1:40;
then A67: ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p1)) `1 = - 1 by A8, A18, A19, JGRAPH_4:47, JGRAPH_4:49;
A68: 1 ^2 = ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)) `1) ^2) + ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)) `2) ^2) by A64, JGRAPH_3:1;
0 < (((p1 `2) -FanMorphW) . p4) `2 by A8, A11, A12, A18, A21, A59, A19, A60, JGRAPH_4:44;
then A69: ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `1 < ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)) `1 by A40, A47, A28, A32, A43, A65, A62, JGRAPH_4:79;
then (((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)) `1) ^2 > (((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `1) ^2 by A51, A56, SQUARE_1:16;
then (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) ^2) - ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)) `2) ^2)) + ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)) `2) ^2) > 0 + ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)) `2) ^2) by A63, A68, XREAL_1:8;
then A70: ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2 > ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)) `2 by A41, SQUARE_1:48;
set s4 = ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4));
set s1 = ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p1));
((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p1)) `2 = 0 by A19, JGRAPH_4:49;
then A71: (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p1))) `2 = 0 by A67, JGRAPH_4:82;
set t4 = (((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1) -FanMorphS) . (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)));
set s3 = ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3));
set s2 = ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2));
A72: |.(((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3))).| ^2 = (((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3))) `1) ^2) + (((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3))) `2) ^2) by JGRAPH_3:1;
A73: (((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) / |.((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)).| = ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2 by A42;
then A74: (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3))) `2 = 0 by A51, A56, JGRAPH_4:111;
|.((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2)).| ^2 = ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2)) `1) ^2) + ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2)) `2) ^2) by JGRAPH_3:1;
then A75: ( ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2)) `2 = - 1 or ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2)) `2 = 1 ) by A52, A51, SQUARE_1:40;
then (((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2) = |[0,1]| by A19, A27, A50, A51, EUCLID:53, JGRAPH_4:80;
then A76: ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2)) = |[0,1]| by A51, JGRAPH_4:82;
(((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2))) `2 = 1 by A19, A27, A50, A51, A75, JGRAPH_4:80, JGRAPH_4:82;
then A77: (((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1) -FanMorphS) . (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p2))) = |[0,1]| by A76, JGRAPH_4:113;
A78: ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2 < 1 by A42, A51, A54, Th2;
then consider f3 being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A79: f3 = (((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE and
A80: f3 is being_homeomorphism by A55, JGRAPH_4:105;
A81: dom (f2 * f1) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A82: (((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)) `2) / |.((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)).| = ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)) `2 by A64;
then A83: ((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3))) `2) / |.(((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3))).| > ((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `2) / |.(((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))).| by A51, A56, A69, A70, A55, A78, A73, JGRAPH_4:110;
A84: |.(((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))).| = 1 by A64, JGRAPH_4:97;
then A85: ((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1) / |.(((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))).| = (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1 ;
then A86: ((((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1) -FanMorphS) . (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)))) `1 = 0 by A84, A74, A83, JGRAPH_4:142;
(((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `2 < 0 by A51, A56, A69, A70, A55, A82, JGRAPH_4:107;
then A87: (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1 < 1 by A84, Th2;
- 1 < (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1 by A51, A56, A69, A70, A55, A82, JGRAPH_4:107;
then consider f4 being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A88: f4 = ((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1) -FanMorphS and
A89: f4 is being_homeomorphism by A87, JGRAPH_4:136;
reconsider g = f4 * (f3 * (f2 * f1)) as Function of (TOP-REAL 2),(TOP-REAL 2) ;
A90: dom (f3 * (f2 * f1)) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
f2 * f1 is being_homeomorphism by A46, A49, TOPS_2:57;
then f3 * (f2 * f1) is being_homeomorphism by A80, TOPS_2:57;
then A91: g is being_homeomorphism by A89, TOPS_2:57;
A92: dom g = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A93: g . p2 = f4 . ((f3 * (f2 * f1)) . p2) by FUNCT_1:12
.= f4 . (f3 . ((f2 * f1) . p2)) by A90, FUNCT_1:12
.= |[0,1]| by A45, A48, A79, A88, A77, A81, FUNCT_1:12 ;
|.(((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3))).| = 1 by A42, JGRAPH_4:97;
then ( (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3))) `1 = - 1 or (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3))) `1 = 1 ) by A74, A72, SQUARE_1:40;
then ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) = |[1,0]| by A51, A56, A73, A74, EUCLID:53, JGRAPH_4:111;
then A94: (((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1) -FanMorphS) . (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3))) = |[1,0]| by A74, JGRAPH_4:113;
((p1 `2) -FanMorphW) . p1 = |[(- 1),0]| by A8, A18, A19, A66, EUCLID:53, JGRAPH_4:47;
then (((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p1) = |[(- 1),0]| by A19, JGRAPH_4:49;
then ((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p1)) = |[(- 1),0]| by A67, JGRAPH_4:82;
then A95: (((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1) -FanMorphS) . (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p1))) = |[(- 1),0]| by A71, JGRAPH_4:113;
A96: |.((((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1) -FanMorphS) . (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)))).| ^2 = ((((((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1) -FanMorphS) . (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)))) `1) ^2) + ((((((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1) -FanMorphS) . (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)))) `2) ^2) by JGRAPH_3:1;
|.((((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1) -FanMorphS) . (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)))).| = 1 by A84, JGRAPH_4:128;
then ( ((((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1) -FanMorphS) . (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)))) `2 = - 1 or ((((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1) -FanMorphS) . (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4)))) `2 = 1 ) by A86, A96, SQUARE_1:40;
then A97: (((((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) `1) -FanMorphS) . (((((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p3)) `2) -FanMorphE) . ((((((p1 `2) -FanMorphW) . p2) `1) -FanMorphN) . (((p1 `2) -FanMorphW) . p4))) = |[0,(- 1)]| by A84, A74, A83, A85, A86, EUCLID:53, JGRAPH_4:142;
A98: for q being Point of (TOP-REAL 2) holds |.(g . q).| = |.q.|

let q be Point of (TOP-REAL 2); :: thesis:
A99: |.((f2 * f1) . q).| = |.(f2 . (f1 . q)).| by A81, FUNCT_1:12
.= |.(f1 . q).| by A48, JGRAPH_4:66
.= |.q.| by A45, JGRAPH_4:33 ;
A100: |.((f3 * (f2 * f1)) . q).| = |.(f3 . ((f2 * f1) . q)).| by A90, FUNCT_1:12
.= |.q.| by A79, A99, JGRAPH_4:97 ;
thus |.(g . q).| = |.(f4 . ((f3 * (f2 * f1)) . q)).| by A92, FUNCT_1:12
.= |.q.| by A88, A100, JGRAPH_4:128 ; :: thesis:

end;

A101: g . p3 = f4 . ((f3 * (f2 * f1)) . p3) by A92, FUNCT_1:12
.= f4 . (f3 . ((f2 * f1) . p3)) by A90, FUNCT_1:12
.= |[1,0]| by A45, A48, A79, A88, A94, A81, FUNCT_1:12 ;
A102: g . p4 = f4 . ((f3 * (f2 * f1)) . p4) by A92, FUNCT_1:12
.= f4 . (f3 . ((f2 * f1) . p4)) by A90, FUNCT_1:12
.= |[0,(- 1)]| by A45, A48, A79, A88, A97, A81, FUNCT_1:12 ;
g . p1 = f4 . ((f3 * (f2 * f1)) . p1) by A92, FUNCT_1:12
.= f4 . (f3 . ((f2 * f1) . p1)) by A90, FUNCT_1:12
.= |[(- 1),0]| by A45, A48, A79, A88, A95, A81, FUNCT_1:12 ;
hence ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & |[(- 1),0]| = f . p1 & |[0,1]| = f . p2 & |[1,0]| = f . p3 & |[0,(- 1)]| = f . p4 ) by A91, A98, A93, A101, A102; :: thesis: