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 -FanMorphW) . q1 & p2 = (sn -FanMorphW) . 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 -FanMorphW) . q1 & p2 = (sn -FanMorphW) . q2 holds
(p1 `2) / |.p1.| < (p2 `2) / |.p2.| )
assume that
A1: - 1 < sn and
A2: sn < 1 and
A3: q1 `1 < 0 and
A4: q2 `1 < 0 and
A5: (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.|
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
A6: p1 = (sn -FanMorphW) . q1 and
A7: p2 = (sn -FanMorphW) . q2 ; :: thesis: (p1 `2) / |.p1.| < (p2 `2) / |.p2.|
now :: thesis: ( ( (q1 `2) / |.q1.| >= sn & (q2 `2) / |.q2.| >= sn & (p1 `2) / |.p1.| < (p2 `2) / |.p2.| ) or ( (q1 `2) / |.q1.| >= sn & (q2 `2) / |.q2.| < sn & (p1 `2) / |.p1.| < (p2 `2) / |.p2.| ) or ( (q1 `2) / |.q1.| < sn & (q2 `2) / |.q2.| >= sn & (p1 `2) / |.p1.| < (p2 `2) / |.p2.| ) or ( (q1 `2) / |.q1.| < sn & (q2 `2) / |.q2.| < sn & (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 ) ) ;
case ( (q1 `2) / |.q1.| >= sn & (q2 `2) / |.q2.| >= sn ) ; :: thesis: (p1 `2) / |.p1.| < (p2 `2) / |.p2.|
hence (p1 `2) / |.p1.| < (p2 `2) / |.p2.| by A2, A3, A4, A5, A6, A7, Th44; :: thesis: verum
end;
case ( (q1 `2) / |.q1.| >= sn & (q2 `2) / |.q2.| < sn ) ; :: thesis: (p1 `2) / |.p1.| < (p2 `2) / |.p2.|
hence (p1 `2) / |.p1.| < (p2 `2) / |.p2.| by A5, XXREAL_0:2; :: thesis: verum
end;
case A8: ( (q1 `2) / |.q1.| < sn & (q2 `2) / |.q2.| >= sn ) ; :: thesis: (p1 `2) / |.p1.| < (p2 `2) / |.p2.|
then p2 `2 >= 0 by A2, A4, A7, Th42;
then A9: (p2 `2) / |.p2.| >= 0 ;
p1 `2 < 0 by A1, A3, A6, A8, Th43;
hence (p1 `2) / |.p1.| < (p2 `2) / |.p2.| by A9, Lm1, JGRAPH_2:3, XREAL_1:141; :: thesis: verum
end;
case ( (q1 `2) / |.q1.| < sn & (q2 `2) / |.q2.| < sn ) ; :: thesis: (p1 `2) / |.p1.| < (p2 `2) / |.p2.|
hence (p1 `2) / |.p1.| < (p2 `2) / |.p2.| by A1, A3, A4, A5, A6, A7, Th45; :: thesis: verum
end;
end;
end;
hence (p1 `2) / |.p1.| < (p2 `2) / |.p2.| ; :: thesis: verum