theorem Th20: :: JGRAPH_5:20

for cn being Real
for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 >= 0 & (q `1) / |.q.| < cn & |.q.| <> 0 holds
for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds
( p `2 >= 0 & p `1 < 0 )