theorem Th137: :: JGRAPH_4:137

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