let cn be Real; :: thesis:
let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis:
let P be non empty compact Subset of (TOP-REAL 2); :: thesis:
assume that
A1: ( - 1 < cn & cn < 1 ) and
A2: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } and
A3: LE p1,p2,P and
A4: q1 = (cn -FanMorphS) . p1 and
A5: q2 = (cn -FanMorphS) . p2 ; :: thesis:
A6: P is being_simple_closed_curve by A2, JGRAPH_3:26;
W-min P = |[(- 1),0]| by A2, Th29;
then A7: (W-min P) `2 = 0 by EUCLID:52;
then A8: (cn -FanMorphS) . (W-min P) = W-min P by JGRAPH_4:113;
p2 in the carrier of (TOP-REAL 2) ;
then A9: p2 in dom (cn -FanMorphS) by FUNCT_2:def 1;
W-min P in the carrier of (TOP-REAL 2) ;
then A10: W-min P in dom (cn -FanMorphS) by FUNCT_2:def 1;
A11: Lower_Arc P c= P by A2, Th33;
A12: cn -FanMorphS is one-to-one by A1, JGRAPH_4:133;
A13: Upper_Arc P c= P by A2, Th33;

A14: now :: thesis:

per cases by A3;

case p1 in Upper_Arc P ; :: thesis:

hence p1 in P by A13; :: thesis:

end;

case p1 in Lower_Arc P ; :: thesis:

hence p1 in P by A11; :: thesis:

end;

end;

end;

A15: now :: thesis:

assume A16: q2 = W-min P ; :: thesis:
then p2 = W-min P by A5, A8, A10, A9, A12, FUNCT_1:def 4;
then LE p2,p1,P by A6, A14, JORDAN7:3;
then A17: q1 = q2 by A2, A3, A4, A5, JGRAPH_3:26, JORDAN6:57;
W-min P in Lower_Arc P by A6, JORDAN7:1;
then LE q1,q2,P by A2, A11, A16, A17, JGRAPH_3:26, JORDAN6:56;
hence ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) ; :: thesis:

end;

A18: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A2, Th34;
A19: Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A2, Th35;

per cases by A3;

suppose A20: ( p1 in Upper_Arc P & p2 in Lower_Arc P & not p2 = W-min P ) ; :: thesis:

A21: |.q2.| = |.p2.| by A5, JGRAPH_4:128;
A22: ex p9 being Point of (TOP-REAL 2) st
( p9 = p2 & p9 in P & p9 `2 <= 0 ) by A19, A20;
then ex p10 being Point of (TOP-REAL 2) st
( p10 = p2 & |.p10.| = 1 ) by A2;
then A23: q2 in P by A2, A21;
A24: ex p8 being Point of (TOP-REAL 2) st
( p8 = p1 & p8 in P & p8 `2 >= 0 ) by A18, A20;
q2 `2 <= 0 by A1, A5, A22, Th57;
hence ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) by A4, A19, A15, A20, A24, A23, JGRAPH_4:113; :: according to JORDAN6:def 10 :: thesis:

end;

suppose A25: ( p1 in Upper_Arc P & p2 in Upper_Arc P & LE p1,p2, Upper_Arc P, W-min P, E-max P ) ; :: thesis:

then ex p8 being Point of (TOP-REAL 2) st
( p8 = p1 & p8 in P & p8 `2 >= 0 ) by A18;
then A26: p1 = (cn -FanMorphS) . p1 by JGRAPH_4:113;
ex p9 being Point of (TOP-REAL 2) st
( p9 = p2 & p9 in P & p9 `2 >= 0 ) by A18, A25;
hence ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) by A4, A5, A25, A26, JGRAPH_4:113; :: according to JORDAN6:def 10 :: thesis:

end;

suppose A27: ( p1 in Lower_Arc P & p2 in Lower_Arc P & not p2 = W-min P & LE p1,p2, Lower_Arc P, E-max P, W-min P & not p1 in Upper_Arc P ) ; :: thesis:

then A28: ex p8 being Point of (TOP-REAL 2) st
( p8 = p1 & p8 in P & p8 `2 <= 0 ) by A19;
then A29: ex p10 being Point of (TOP-REAL 2) st
( p10 = p1 & |.p10.| = 1 ) by A2;
A30: ex p9 being Point of (TOP-REAL 2) st
( p9 = p2 & p9 in P & p9 `2 <= 0 ) by A19, A27;
then A31: ex p11 being Point of (TOP-REAL 2) st
( p11 = p2 & |.p11.| = 1 ) by A2;
A32: q2 `2 <= 0 by A1, A5, A30, Th57;
A33: |.q2.| = |.p2.| by A5, JGRAPH_4:128;
then A34: q2 in P by A2, A31;
A35: q1 `2 <= 0 by A1, A4, A28, Th57;
A36: |.q1.| = |.p1.| by A4, JGRAPH_4:128;
then A37: q1 in P by A2, A29;

now :: thesis:

per cases ;

case A38: p1 = W-min P ; :: thesis:

then p1 = (cn -FanMorphS) . p1 by A7, JGRAPH_4:113;
then LE q1,q2,P by A4, A6, A34, A38, JORDAN7:3;
hence ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) ; :: thesis:

end;

case A39: p1 <> W-min P ; :: thesis:

now :: thesis:

per cases by A2, A3, A28, A39, Th48;

case A40: p1 `1 = p2 `1 ; :: thesis:

A41: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;

A42: now :: thesis:

assume A43: p1 `2 = - (p2 `2) ; :: thesis:
then p2 `2 = 0 by A28, A30, XREAL_1:58;
hence p1 = p2 by A40, A41, A43, EUCLID:53; :: thesis:

end;

((p1 `1) ^2) + ((p1 `2) ^2) = 1 ^2 by A29, JGRAPH_3:1
.= ((p1 `1) ^2) + ((p2 `2) ^2) by A31, A40, JGRAPH_3:1 ;
then A44: ( p1 `2 = p2 `2 or p1 `2 = - (p2 `2) ) by SQUARE_1:40;
p1 = |[(p1 `1),(p1 `2)]| by EUCLID:53;
then LE q1,q2,P by A2, A4, A5, A34, A40, A44, A41, A42, JGRAPH_3:26, JORDAN6:56;
hence ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) ; :: thesis:

end;

case p1 `1 > p2 `1 ; :: thesis:

then (p1 `1) / |.p1.| > (p2 `1) / |.p2.| by A29, A31;
then A45: (q1 `1) / |.q1.| >= (q2 `1) / |.q2.| by A1, A4, A5, A28, A30, A29, A31, Th27;
q2 <> W-min P by A5, A8, A10, A9, A12, A27, FUNCT_1:def 4;
then LE q1,q2,P by A2, A36, A33, A35, A32, A29, A31, A37, A34, A45, Th56;
hence ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) ; :: thesis:

end;

end;

end;

hence ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) ; :: thesis:

end;

end;

end;

hence ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) ; :: according to JORDAN6:def 10 :: thesis:

end;

end;