theorem Th25: :: JGRAPH_5:25

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