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 that
A1: ( - 1 < cn & cn < 1 ) and
A2: q1 `2 <= 0 and
A3: q2 `2 <= 0 and
A4: |.q1.| <> 0 and
A5: |.q2.| <> 0 and
A6: (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 A2;

case A7: 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 A3;

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, A6, A7, JGRAPH_4:148; :: thesis: verum

end;

case A8: 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.|

A9: now

|.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 by SQUARE_1:117;
then A10: (- |.q1.|) / |.q1.| <= (q1 `1) / |.q1.| by XREAL_1:74;
assume |.q2.| = - (q2 `1) ; :: thesis: contradiction
then 1 = (- (q2 `1)) / |.q2.| by A5, XCMPLX_1:60;
then (q1 `1) / |.q1.| < - 1 by A6, XCMPLX_1:191;
hence contradiction by A4, A10, XCMPLX_1:198; :: thesis: verum

end;

|.q2.| ^2 = ((q2 `1) ^2) + (0 ^2) by A8, JGRAPH_3:10
.= (q2 `1) ^2 ;
then ( |.q2.| = q2 `1 or |.q2.| = - (q2 `1) ) by SQUARE_1:109;
then A11: (q2 `1) / |.q2.| = 1 by A5, A9, 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 that
A12: p1 = (cn -FanMorphS) . q1 and
A13: p2 = (cn -FanMorphS) . q2 ; :: thesis: (p1 `1) / |.p1.| < (p2 `1) / |.p2.|
A14: |.p1.| = |.q1.| by A12, JGRAPH_4:135;
A15: |.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by JGRAPH_3:10;
A16: p1 `2 < 0 by A1, A7, A12, Th28;

A17: now

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

end;

A18: p2 = q2 by A8, A13, JGRAPH_4:120;
(|.p1.| ^2) - ((p1 `1) ^2) >= 0 by A15, XREAL_1:65;
then ((|.p1.| ^2) - ((p1 `1) ^2)) + ((p1 `1) ^2) >= 0 + ((p1 `1) ^2) by XREAL_1:9;
then p1 `1 <= |.p1.| by SQUARE_1:117;
then |.p1.| / |.p1.| >= (p1 `1) / |.p1.| by XREAL_1:74;
then 1 >= (p1 `1) / |.p1.| by A4, A14, XCMPLX_1:60;
hence (p1 `1) / |.p1.| < (p2 `1) / |.p2.| by A11, A18, A17, 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 A19: 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.|

A20: now

|.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 `1 <= |.q2.| by SQUARE_1:117;
then A21: |.q2.| / |.q2.| >= (q2 `1) / |.q2.| by XREAL_1:74;
assume |.q1.| = q1 `1 ; :: thesis: contradiction
then (q2 `1) / |.q2.| > 1 by A4, A6, XCMPLX_1:60;
hence contradiction by A5, A21, XCMPLX_1:60; :: thesis: verum

end;

|.q1.| ^2 = ((q1 `1) ^2) + (0 ^2) by A19, JGRAPH_3:10
.= (q1 `1) ^2 ;
then ( |.q1.| = q1 `1 or |.q1.| = - (q1 `1) ) by SQUARE_1:109;
then (- (q1 `1)) / |.q1.| = 1 by A4, A20, XCMPLX_1:60;
then A22: - ((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 that
A23: p1 = (cn -FanMorphS) . q1 and
A24: p2 = (cn -FanMorphS) . q2 ; :: thesis: (p1 `1) / |.p1.| < (p2 `1) / |.p2.|
A25: |.p2.| = |.q2.| by A24, JGRAPH_4:135;
A26: |.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 by SQUARE_1:117;
then (- |.p2.|) / |.p2.| <= (p2 `1) / |.p2.| by XREAL_1:74;
then A27: - 1 <= (p2 `1) / |.p2.| by A5, A25, XCMPLX_1:198;

A28: now

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

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

then p2 = q2 by A24, JGRAPH_4:120;
hence (p2 `1) / |.p2.| > - 1 by A6, A22; :: thesis: verum

end;

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

then A29: p2 `2 < 0 by A1, A3, A24, Th28;

now

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

end;

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

end;

end;

end;

p1 = q1 by A19, A23, JGRAPH_4:120;
hence (p1 `1) / |.p1.| < (p2 `1) / |.p2.| by A22, A28; :: 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