let cn be Real; :: thesis: for q1, q2 being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q1 `2 <= 0 & q2 `2 <= 0 & |.q1.| <> 0 & |.q2.| <> 0 & (q1 `1 ) / |.q1.| < (q2 `1 ) / |.q2.| holds
for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 holds
(p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.|
let q1, q2 be Point of (TOP-REAL 2); :: thesis: ( - 1 < cn & cn < 1 & q1 `2 <= 0 & q2 `2 <= 0 & |.q1.| <> 0 & |.q2.| <> 0 & (q1 `1 ) / |.q1.| < (q2 `1 ) / |.q2.| implies for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 holds
(p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.| )
assume A1: ( - 1 < cn & cn < 1 & q1 `2 <= 0 & q2 `2 <= 0 & |.q1.| <> 0 & |.q2.| <> 0 & (q1 `1 ) / |.q1.| < (q2 `1 ) / |.q2.| ) ; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 holds
(p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.|

now

per cases ( q1 `2 < 0 or q1 `2 = 0 ) by A1;

case A2: q1 `2 < 0 ; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 holds
(p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.|

now

per cases ( q2 `2 < 0 or q2 `2 = 0 ) by A1;

case q2 `2 < 0 ; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 holds
(p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.|

hence for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 holds
(p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.| by A1, A2, JGRAPH_4:148; :: thesis: verum

end;

case A3: q2 `2 = 0 ; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 holds
(p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.|

then |.q2.| ^2 = ((q2 `1 ) ^2 ) + (0 ^2 ) by JGRAPH_3:10
.= (q2 `1 ) ^2 ;
then A4: ( |.q2.| = q2 `1 or |.q2.| = - (q2 `1 ) ) by SQUARE_1:109;

now

assume |.q2.| = - (q2 `1 ) ; :: thesis: contradiction
then 1 = (- (q2 `1 )) / |.q2.| by A1, XCMPLX_1:60;
then A5: (q1 `1 ) / |.q1.| < - 1 by A1, XCMPLX_1:191;
|.q1.| ^2 = ((q1 `1 ) ^2 ) + ((q1 `2 ) ^2 ) by JGRAPH_3:10;
then (|.q1.| ^2 ) - ((q1 `1 ) ^2 ) >= 0 by XREAL_1:65;
then ((|.q1.| ^2 ) - ((q1 `1 ) ^2 )) + ((q1 `1 ) ^2 ) >= 0 + ((q1 `1 ) ^2 ) by XREAL_1:9;
then ( - |.q1.| <= q1 `1 & q1 `1 <= |.q1.| ) by SQUARE_1:117;
then (- |.q1.|) / |.q1.| <= (q1 `1 ) / |.q1.| by XREAL_1:74;
hence contradiction by A1, A5, XCMPLX_1:198; :: thesis: verum

end;

then A7: (q2 `1 ) / |.q2.| = 1 by A1, A4, XCMPLX_1:60;
thus for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 holds
(p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.| :: thesis: verum

proof

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 implies (p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.| )
assume A8: ( p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 ) ; :: thesis: (p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.|
then A9: p2 = q2 by A3, JGRAPH_4:120;
A10: |.p1.| = |.q1.| by A8, JGRAPH_4:135;
A12: |.p1.| ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) by JGRAPH_3:10;
then (|.p1.| ^2 ) - ((p1 `1 ) ^2 ) >= 0 by XREAL_1:65;
then ((|.p1.| ^2 ) - ((p1 `1 ) ^2 )) + ((p1 `1 ) ^2 ) >= 0 + ((p1 `1 ) ^2 ) by XREAL_1:9;
then ( - |.p1.| <= p1 `1 & p1 `1 <= |.p1.| ) by SQUARE_1:117;
then |.p1.| / |.p1.| >= (p1 `1 ) / |.p1.| by XREAL_1:74;
then A13: 1 >= (p1 `1 ) / |.p1.| by A1, A10, XCMPLX_1:60;
A14: p1 `2 < 0 by A1, A2, A8, Th28;

now

assume 1 = (p1 `1 ) / |.p1.| ; :: thesis: contradiction
then 1 * |.p1.| = p1 `1 by A1, A10, XCMPLX_1:88;
hence contradiction by A12, A14, XCMPLX_1:6; :: thesis: verum

end;

hence (p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.| by A7, A9, A13, XXREAL_0:1; :: thesis: verum

end;

end;

end;

end;

hence for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 holds
(p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.| ; :: thesis: verum

end;

case A15: q1 `2 = 0 ; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 holds
(p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.|

then |.q1.| ^2 = ((q1 `1 ) ^2 ) + (0 ^2 ) by JGRAPH_3:10
.= (q1 `1 ) ^2 ;
then A16: ( |.q1.| = q1 `1 or |.q1.| = - (q1 `1 ) ) by SQUARE_1:109;

now

assume |.q1.| = q1 `1 ; :: thesis: contradiction
then A17: (q2 `1 ) / |.q2.| > 1 by A1, XCMPLX_1:60;
|.q2.| ^2 = ((q2 `1 ) ^2 ) + ((q2 `2 ) ^2 ) by JGRAPH_3:10;
then (|.q2.| ^2 ) - ((q2 `1 ) ^2 ) >= 0 by XREAL_1:65;
then ((|.q2.| ^2 ) - ((q2 `1 ) ^2 )) + ((q2 `1 ) ^2 ) >= 0 + ((q2 `1 ) ^2 ) by XREAL_1:9;
then ( - |.q2.| <= q2 `1 & q2 `1 <= |.q2.| ) by SQUARE_1:117;
then |.q2.| / |.q2.| >= (q2 `1 ) / |.q2.| by XREAL_1:74;
hence contradiction by A1, A17, XCMPLX_1:60; :: thesis: verum

end;

then (- (q1 `1 )) / |.q1.| = 1 by A1, A16, XCMPLX_1:60;
then A19: - ((q1 `1 ) / |.q1.|) = 1 by XCMPLX_1:188;
thus for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 holds
(p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.| :: thesis: verum

proof

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 implies (p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.| )
assume A20: ( p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 ) ; :: thesis: (p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.|
then A21: p1 = q1 by A15, JGRAPH_4:120;
A22: |.p2.| = |.q2.| by A20, JGRAPH_4:135;
A24: |.p2.| ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) by JGRAPH_3:10;
then (|.p2.| ^2 ) - ((p2 `1 ) ^2 ) >= 0 by XREAL_1:65;
then ((|.p2.| ^2 ) - ((p2 `1 ) ^2 )) + ((p2 `1 ) ^2 ) >= 0 + ((p2 `1 ) ^2 ) by XREAL_1:9;
then ( - |.p2.| <= p2 `1 & p2 `1 <= |.p2.| ) by SQUARE_1:117;
then (- |.p2.|) / |.p2.| <= (p2 `1 ) / |.p2.| by XREAL_1:74;
then A25: - 1 <= (p2 `1 ) / |.p2.| by A1, A22, XCMPLX_1:198;

now

per cases ( q2 `2 = 0 or q2 `2 <> 0 ) ;

case q2 `2 = 0 ; :: thesis: (p2 `1 ) / |.p2.| > - 1

then p2 = q2 by A20, JGRAPH_4:120;
hence (p2 `1 ) / |.p2.| > - 1 by A1, A19; :: thesis: verum

end;

case q2 `2 <> 0 ; :: thesis: (p2 `1 ) / |.p2.| > - 1

then A26: p2 `2 < 0 by A1, A20, Th28;

now

assume - 1 = (p2 `1 ) / |.p2.| ; :: thesis: contradiction
then (- 1) * |.p2.| = p2 `1 by A1, A22, XCMPLX_1:88;
then |.p2.| ^2 = (p2 `1 ) ^2 ;
hence contradiction by A24, A26, XCMPLX_1:6; :: thesis: verum

end;

hence (p2 `1 ) / |.p2.| > - 1 by A25, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence (p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.| by A19, A21; :: thesis: verum

end;

end;

end;

end;

hence for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 holds
(p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.| ; :: thesis: verum