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 `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 `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 `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.|
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 A2: ( p1 = (cn -FanMorphS ) . q1 & p2 = (cn -FanMorphS ) . q2 ) ; :: thesis: (p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.|
per cases ( ( (q1 `1 ) / |.q1.| >= cn & (q2 `1 ) / |.q2.| >= cn ) or ( (q1 `1 ) / |.q1.| >= cn & (q2 `1 ) / |.q2.| < cn ) or ( (q1 `1 ) / |.q1.| < cn & (q2 `1 ) / |.q2.| >= cn ) or ( (q1 `1 ) / |.q1.| < cn & (q2 `1 ) / |.q2.| < cn ) ) ;
suppose ( (q1 `1 ) / |.q1.| >= cn & (q2 `1 ) / |.q2.| >= cn ) ; :: thesis: (p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.|
hence (p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.| by A1, A2, Th146; :: thesis: verum
end;
suppose ( (q1 `1 ) / |.q1.| >= cn & (q2 `1 ) / |.q2.| < cn ) ; :: thesis: (p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.|
hence (p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.| by A1, XXREAL_0:2; :: thesis: verum
end;
suppose A3: ( (q1 `1 ) / |.q1.| < cn & (q2 `1 ) / |.q2.| >= cn ) ; :: thesis: (p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.|
then A4: ( p1 `2 < 0 & p1 `1 < 0 ) by A1, A2, Th145;
then A5: |.p1.| > 0 by Lm1, JGRAPH_2:11;
( p2 `2 < 0 & p2 `1 >= 0 ) by A1, A2, A3, Th144;
then (p2 `1 ) / |.p2.| >= 0 ;
hence (p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.| by A4, A5, XREAL_1:143; :: thesis: verum
end;
suppose ( (q1 `1 ) / |.q1.| < cn & (q2 `1 ) / |.q2.| < cn ) ; :: thesis: (p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.|
hence (p1 `1 ) / |.p1.| < (p2 `1 ) / |.p2.| by A1, A2, Th147; :: thesis: verum
end;
end;