let cn be Real; for q1, q2 being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q1 `2 <= 0 & q2 `2 <= 0 & |.q1.| <> 0 & |.q2.| <> 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); ( - 1 < cn & cn < 1 & q1 `2 <= 0 & q2 `2 <= 0 & |.q1.| <> 0 & |.q2.| <> 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 that
A1:
( - 1 < cn & cn < 1 )
and
A2:
q1 `2 <= 0
and
A3:
q2 `2 <= 0
and
A4:
|.q1.| <> 0
and
A5:
|.q2.| <> 0
and
A6:
(q1 `1) / |.q1.| < (q2 `1) / |.q2.|
; 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.|
now ( ( q1 `2 < 0 & ( 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.| ) ) or ( q1 `2 = 0 & ( 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.| ) ) )per cases
( q1 `2 < 0 or q1 `2 = 0 )
by A2;
case A7:
q1 `2 < 0
;
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.|now ( ( q2 `2 < 0 & ( 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.| ) ) or ( q2 `2 = 0 & ( 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.| ) ) )per cases
( q2 `2 < 0 or q2 `2 = 0 )
by A3;
case A8:
q2 `2 = 0
;
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.||.q2.| ^2 =
((q2 `1) ^2) + (0 ^2)
by A8, JGRAPH_3:1
.=
(q2 `1) ^2
;
then
(
|.q2.| = q2 `1 or
|.q2.| = - (q2 `1) )
by SQUARE_1:40;
then A11:
(q2 `1) / |.q2.| = 1
by A5, A9, XCMPLX_1:60;
thus
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.|
verumproof
let p1,
p2 be
Point of
(TOP-REAL 2);
( p1 = (cn -FanMorphS) . q1 & p2 = (cn -FanMorphS) . q2 implies (p1 `1) / |.p1.| < (p2 `1) / |.p2.| )
assume that A12:
p1 = (cn -FanMorphS) . q1
and A13:
p2 = (cn -FanMorphS) . q2
;
(p1 `1) / |.p1.| < (p2 `1) / |.p2.|
A14:
|.p1.| = |.q1.|
by A12, JGRAPH_4:128;
A15:
|.p1.| ^2 = ((p1 `1) ^2) + ((p1 `2) ^2)
by JGRAPH_3:1;
A16:
p1 `2 < 0
by A1, A7, A12, Th25;
A18:
p2 = q2
by A8, A13, JGRAPH_4:113;
(|.p1.| ^2) - ((p1 `1) ^2) >= 0
by A15, XREAL_1:63;
then
((|.p1.| ^2) - ((p1 `1) ^2)) + ((p1 `1) ^2) >= 0 + ((p1 `1) ^2)
by XREAL_1:7;
then
p1 `1 <= |.p1.|
by SQUARE_1:47;
then
|.p1.| / |.p1.| >= (p1 `1) / |.p1.|
by XREAL_1:72;
then
1
>= (p1 `1) / |.p1.|
by A4, A14, XCMPLX_1:60;
hence
(p1 `1) / |.p1.| < (p2 `1) / |.p2.|
by A11, A18, A17, XXREAL_0:1;
verum
end; end; end; end; hence
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.|
;
verum end; end; end;
hence
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.|
; verum