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 that
A1: - 1 < cn and
A2: cn < 1 and
A3: 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 A4: p = (cn -FanMorphS) . q ; :: thesis: p `2 <= 0

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

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

now :: thesis: ( ( (q `1) / |.q.| < cn & p `2 <= 0 ) or ( (q `1) / |.q.| >= cn & p `2 <= 0 ) )

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, A4, A5, JGRAPH_4:138; :: thesis: verum

end;

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

hence p `2 <= 0 by A2, A4, A5, JGRAPH_4:137; :: 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 A4, JGRAPH_4:113; :: thesis: verum

end;

end;