let cn be Real; :: thesis: 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
let q be Point of (TOP-REAL 2); :: thesis: ( - 1 < cn & cn < 1 & q `2 <= 0 implies for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS ) . q holds
p `2 <= 0 )
assume A1: ( - 1 < cn & cn < 1 & q `2 <= 0 ) ; :: thesis: for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS ) . q holds
p `2 <= 0
let p be Point of (TOP-REAL 2); :: thesis: ( p = (cn -FanMorphS ) . q implies p `2 <= 0 )
assume A2: p = (cn -FanMorphS ) . q ; :: thesis: p `2 <= 0

per cases ( q `2 < 0 or q `2 = 0 ) by A1;

suppose A3: q `2 < 0 ; :: thesis: p `2 <= 0

now

per cases ( (q `1 ) / |.q.| < cn or (q `1 ) / |.q.| >= cn ) ;

case (q `1 ) / |.q.| < cn ; :: thesis: p `2 <= 0

hence p `2 <= 0 by A1, A2, A3, JGRAPH_4:145; :: thesis: verum

end;

case (q `1 ) / |.q.| >= cn ; :: thesis: p `2 <= 0

hence p `2 <= 0 by A1, A2, A3, JGRAPH_4:144; :: thesis: verum

end;

end;

end;

hence p `2 <= 0 ; :: thesis: verum

end;

suppose q `2 = 0 ; :: thesis: p `2 <= 0

hence p `2 <= 0 by A2, JGRAPH_4:120; :: thesis: verum

end;

end;