theorem :: JGRAPH_4:80

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