let sn be Real; 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); ( - 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 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.|
; 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); ( p1 = (sn -FanMorphE) . q1 & p2 = (sn -FanMorphE) . q2 implies (p1 `2) / |.p1.| < (p2 `2) / |.p2.| )
assume that
A6:
p1 = (sn -FanMorphE) . q1
and
A7:
p2 = (sn -FanMorphE) . q2
; (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 A8:
(
(q1 `2) / |.q1.| < sn &
(q2 `2) / |.q2.| >= sn )
;
(p1 `2) / |.p1.| < (p2 `2) / |.p2.|then
p2 `2 >= 0
by A2, A4, A7, Th106;
then A9:
(p2 `2) / |.p2.| >= 0
;
p1 `2 < 0
by A1, A3, A6, A8, Th107;
hence
(p1 `2) / |.p1.| < (p2 `2) / |.p2.|
by A9, Lm1, JGRAPH_2:3, XREAL_1:141;
verum end;