let sn be Real; for q1, q2 being Point of (TOP-REAL 2) st - 1 < sn & 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); ( - 1 < sn & 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:
- 1 < sn
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.|
; 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:9, XREAL_1:148;
let p1, p2 be Point of (TOP-REAL 2); ( 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
; (p1 `2) / |.p1.| < (p2 `2) / |.p2.|
A10:
|.p2.| = |.q2.|
by A9, Th33;
p2 = |[(|.q2.| * (- (sqrt (1 - (((((q2 `2) / |.q2.|) - sn) / (1 + sn)) ^2))))),(|.q2.| * ((((q2 `2) / |.q2.|) - sn) / (1 + sn)))]|
by A4, A5, A9, Th17;
then A11:
p2 `2 = |.q2.| * ((((q2 `2) / |.q2.|) - sn) / (1 + sn))
by EUCLID:52;
|.q2.| > 0
by A4, Lm1, JGRAPH_2:3;
then A12:
(p2 `2) / |.p2.| = (((q2 `2) / |.q2.|) - sn) / (1 + sn)
by A11, A10, XCMPLX_1:89;
p1 = |[(|.q1.| * (- (sqrt (1 - (((((q1 `2) / |.q1.|) - sn) / (1 + sn)) ^2))))),(|.q1.| * ((((q1 `2) / |.q1.|) - sn) / (1 + sn)))]|
by A2, A3, A8, Th17;
then A13:
p1 `2 = |.q1.| * ((((q1 `2) / |.q1.|) - sn) / (1 + sn))
by EUCLID:52;
A14:
|.p1.| = |.q1.|
by A8, Th33;
|.q1.| > 0
by A2, Lm1, JGRAPH_2:3;
then
(p1 `2) / |.p1.| = (((q1 `2) / |.q1.|) - sn) / (1 + sn)
by A13, A14, XCMPLX_1:89;
hence
(p1 `2) / |.p1.| < (p2 `2) / |.p2.|
by A12, A7, XREAL_1:74; verum