let sn be Real; :: thesis: for q1, q2 being Point of (TOP-REAL 2) st sn < 1 & q1 `1 < 0 & (q1 `2 ) / |.q1.| >= sn & q2 `1 < 0 & (q2 `2 ) / |.q2.| >= sn & (q1 `2 ) / |.q1.| < (q2 `2 ) / |.q2.| holds
for p1, p2 being Point of (TOP-REAL 2) st p1 = (sn -FanMorphW ) . q1 & p2 = (sn -FanMorphW ) . q2 holds
(p1 `2 ) / |.p1.| < (p2 `2 ) / |.p2.|
let q1, q2 be Point of (TOP-REAL 2); :: thesis: ( sn < 1 & q1 `1 < 0 & (q1 `2 ) / |.q1.| >= sn & q2 `1 < 0 & (q2 `2 ) / |.q2.| >= sn & (q1 `2 ) / |.q1.| < (q2 `2 ) / |.q2.| implies for p1, p2 being Point of (TOP-REAL 2) st p1 = (sn -FanMorphW ) . q1 & p2 = (sn -FanMorphW ) . q2 holds
(p1 `2 ) / |.p1.| < (p2 `2 ) / |.p2.| )
assume that
A1: sn < 1 and
A2: q1 `1 < 0 and
A3: (q1 `2 ) / |.q1.| >= sn and
A4: q2 `1 < 0 and
A5: (q2 `2 ) / |.q2.| >= sn and
A6: (q1 `2 ) / |.q1.| < (q2 `2 ) / |.q2.| ; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 = (sn -FanMorphW ) . q1 & p2 = (sn -FanMorphW ) . q2 holds
(p1 `2 ) / |.p1.| < (p2 `2 ) / |.p2.|
A7: ( ((q1 `2 ) / |.q1.|) - sn < ((q2 `2 ) / |.q2.|) - sn & 1 - sn > 0 ) by A1, A6, XREAL_1:11, XREAL_1:151;
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 = (sn -FanMorphW ) . q1 & p2 = (sn -FanMorphW ) . q2 implies (p1 `2 ) / |.p1.| < (p2 `2 ) / |.p2.| )
assume that
A8: p1 = (sn -FanMorphW ) . q1 and
A9: p2 = (sn -FanMorphW ) . q2 ; :: thesis: (p1 `2 ) / |.p1.| < (p2 `2 ) / |.p2.|
A10: |.p2.| = |.q2.| by A9, Th40;
p2 = |[(|.q2.| * (- (sqrt (1 - (((((q2 `2 ) / |.q2.|) - sn) / (1 - sn)) ^2 ))))),(|.q2.| * ((((q2 `2 ) / |.q2.|) - sn) / (1 - sn)))]| by A4, A5, A9, Th23;
then A11: p2 `2 = |.q2.| * ((((q2 `2 ) / |.q2.|) - sn) / (1 - sn)) by EUCLID:56;
|.q2.| > 0 by A4, Lm1, JGRAPH_2:11;
then A12: (p2 `2 ) / |.p2.| = (((q2 `2 ) / |.q2.|) - sn) / (1 - sn) by A11, A10, XCMPLX_1:90;
p1 = |[(|.q1.| * (- (sqrt (1 - (((((q1 `2 ) / |.q1.|) - sn) / (1 - sn)) ^2 ))))),(|.q1.| * ((((q1 `2 ) / |.q1.|) - sn) / (1 - sn)))]| by A2, A3, A8, Th23;
then A13: p1 `2 = |.q1.| * ((((q1 `2 ) / |.q1.|) - sn) / (1 - sn)) by EUCLID:56;
A14: |.p1.| = |.q1.| by A8, Th40;
|.q1.| > 0 by A2, Lm1, JGRAPH_2:11;
then (p1 `2 ) / |.p1.| = (((q1 `2 ) / |.q1.|) - sn) / (1 - sn) by A13, A14, XCMPLX_1:90;
hence (p1 `2 ) / |.p1.| < (p2 `2 ) / |.p2.| by A12, A7, XREAL_1:76; :: thesis: verum