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 A1: ( - 1 < cn & cn < 1 & P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & q1 = (cn -FanMorphS ) . p1 & q2 = (cn -FanMorphS ) . p2 ) ; :: thesis:
then A2: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by Th37;
A3: Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A1, Th38;
A4: P is being_simple_closed_curve by A1, JGRAPH_3:36;
W-min P = |[(- 1),0 ]| by A1, Th32;
then A5: (W-min P) `2 = 0 by EUCLID:56;
then A6: (cn -FanMorphS ) . (W-min P) = W-min P by JGRAPH_4:120;
W-min P in the carrier of (TOP-REAL 2) ;
then A7: W-min P in dom (cn -FanMorphS ) by FUNCT_2:def 1;
p2 in the carrier of (TOP-REAL 2) ;
then A8: p2 in dom (cn -FanMorphS ) by FUNCT_2:def 1;
A9: cn -FanMorphS is one-to-one by A1, JGRAPH_4:140;
A10: Upper_Arc P c= P by A1, Th36;
A11: Lower_Arc P c= P by A1, Th36;

A12: now

per cases by A1, JORDAN6:def 10;

case p1 in Upper_Arc P ; :: thesis:

hence p1 in P by A10; :: thesis:

end;

case p1 in Lower_Arc P ; :: thesis:

hence p1 in P by A11; :: thesis:

end;

A13: now

assume A14: q2 = W-min P ; :: thesis:
then p2 = W-min P by A1, A6, A7, A8, A9, FUNCT_1:def 8;
then LE p2,p1,P by A4, A12, JORDAN7:3;
then A15: q1 = q2 by A1, JGRAPH_3:36, JORDAN6:72;
W-min P in Lower_Arc P by A4, JORDAN7:1;
then LE q1,q2,P by A1, A11, A14, A15, JGRAPH_3:36, JORDAN6:71;
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 JORDAN6:def 10; :: thesis:

end;

per cases by A1, JORDAN6:def 10;

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

then consider p8 being Point of (TOP-REAL 2) such that
A17: ( p8 = p1 & p8 in P & p8 `2 >= 0 ) by A2;
consider p9 being Point of (TOP-REAL 2) such that
A18: ( p9 = p2 & p9 in P & p9 `2 <= 0 ) by A3, A16;
A19: |.q2.| = |.p2.| by A1, JGRAPH_4:135;
consider p10 being Point of (TOP-REAL 2) such that
A20: ( p10 = p2 & |.p10.| = 1 ) by A1, A18;
A21: q2 in P by A1, A19, A20;
q2 `2 <= 0 by A1, A18, Th60;
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 A1, A3, A13, A16, A17, A21, JGRAPH_4:120; :: according to JORDAN6:def 10 :: thesis:

end;

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

then consider p8 being Point of (TOP-REAL 2) such that
A23: ( p8 = p1 & p8 in P & p8 `2 >= 0 ) by A2;
consider p9 being Point of (TOP-REAL 2) such that
A24: ( p9 = p2 & p9 in P & p9 `2 >= 0 ) by A2, A22;
p1 = (cn -FanMorphS ) . p1 by A23, JGRAPH_4:120;
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 A1, A22, A24, JGRAPH_4:120; :: according to JORDAN6:def 10 :: thesis:

end;

suppose A25: ( 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:

A26: |.q1.| = |.p1.| by A1, JGRAPH_4:135;
A27: |.q2.| = |.p2.| by A1, JGRAPH_4:135;
consider p8 being Point of (TOP-REAL 2) such that
A28: ( p8 = p1 & p8 in P & p8 `2 <= 0 ) by A3, A25;
A29: q1 `2 <= 0 by A1, A28, Th60;
consider p9 being Point of (TOP-REAL 2) such that
A30: ( p9 = p2 & p9 in P & p9 `2 <= 0 ) by A3, A25;
A31: q2 `2 <= 0 by A1, A30, Th60;
consider p10 being Point of (TOP-REAL 2) such that
A32: ( p10 = p1 & |.p10.| = 1 ) by A1, A28;
consider p11 being Point of (TOP-REAL 2) such that
A33: ( p11 = p2 & |.p11.| = 1 ) by A1, A30;
A34: q1 in P by A1, A26, A32;
A35: q2 in P by A1, A27, A33;

per cases ;

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

then p1 = (cn -FanMorphS ) . p1 by A5, JGRAPH_4:120;
then LE q1,q2,P by A1, A4, A35, A36, 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 ) ) by JORDAN6:def 10; :: thesis:

end;

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

per cases by A1, A28, A30, A37, Th51;

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

((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) = 1 ^2 by A32, JGRAPH_3:10
.= ((p1 `1 ) ^2 ) + ((p2 `2 ) ^2 ) by A33, A38, JGRAPH_3:10 ;
then A39: ( p1 `2 = p2 `2 or p1 `2 = - (p2 `2 ) ) by SQUARE_1:109;
A40: p1 = |[(p1 `1 ),(p1 `2 )]| by EUCLID:57;
A41: p2 = |[(p2 `1 ),(p2 `2 )]| by EUCLID:57;

assume A42: p1 `2 = - (p2 `2 ) ; :: thesis:
then p2 `2 = 0 by A28, A30, XREAL_1:60;
hence p1 = p2 by A38, A41, A42, EUCLID:57; :: thesis:

end;

then LE q1,q2,P by A1, A35, A38, A39, A40, A41, JGRAPH_3:36, JORDAN6:71;
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 JORDAN6:def 10; :: thesis:

end;

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

then A43: (p1 `1 ) / |.p1.| > (p2 `1 ) / |.p2.| by A32, A33;
A44: q2 <> W-min P by A1, A6, A7, A8, A9, A25, FUNCT_1:def 8;
(q1 `1 ) / |.q1.| >= (q2 `1 ) / |.q2.| by A1, A28, A30, A32, A33, A43, Th30;
then LE q1,q2,P by A1, A26, A27, A29, A31, A32, A33, A34, A35, A44, Th59;
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 JORDAN6:def 10; :: thesis:

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;