theorem :: JGRAPH_4:111

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