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

per cases ( ( (q1 `2 ) / |.q1.| >= sn & (q2 `2 ) / |.q2.| >= sn ) or ( (q1 `2 ) / |.q1.| >= sn & (q2 `2 ) / |.q2.| < sn ) or ( (q1 `2 ) / |.q1.| < sn & (q2 `2 ) / |.q2.| >= sn ) or ( (q1 `2 ) / |.q1.| < sn & (q2 `2 ) / |.q2.| < sn ) ) ;

suppose ( (q1 `2 ) / |.q1.| >= sn & (q2 `2 ) / |.q2.| >= sn ) ; :: thesis: (p1 `2 ) / |.p1.| < (p2 `2 ) / |.p2.|

hence (p1 `2 ) / |.p1.| < (p2 `2 ) / |.p2.| by A1, A2, Th115; :: thesis: verum

end;

suppose ( (q1 `2 ) / |.q1.| >= sn & (q2 `2 ) / |.q2.| < sn ) ; :: thesis: (p1 `2 ) / |.p1.| < (p2 `2 ) / |.p2.|

hence (p1 `2 ) / |.p1.| < (p2 `2 ) / |.p2.| by A1, XXREAL_0:2; :: thesis: verum

end;

suppose A3: ( (q1 `2 ) / |.q1.| < sn & (q2 `2 ) / |.q2.| >= sn ) ; :: thesis: (p1 `2 ) / |.p1.| < (p2 `2 ) / |.p2.|

then A4: ( p1 `1 > 0 & p1 `2 < 0 ) by A1, A2, Th114;
then A5: |.p1.| > 0 by Lm1, JGRAPH_2:11;
( p2 `1 > 0 & p2 `2 >= 0 ) by A1, A2, A3, Th113;
then (p2 `2 ) / |.p2.| >= 0 ;
hence (p1 `2 ) / |.p1.| < (p2 `2 ) / |.p2.| by A4, A5, XREAL_1:143; :: thesis: verum

end;

suppose ( (q1 `2 ) / |.q1.| < sn & (q2 `2 ) / |.q2.| < sn ) ; :: thesis: (p1 `2 ) / |.p1.| < (p2 `2 ) / |.p2.|

hence (p1 `2 ) / |.p1.| < (p2 `2 ) / |.p2.| by A1, A2, Th116; :: thesis: verum

end;

end;