theorem Th45: :: JGRAPH_4:45

for sn being 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.|