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

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

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

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

hence for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds
p `2 < 0 by A2, A3, JGRAPH_4:137; :: thesis: verum

end;

case (q `1) / |.q.| < cn ; :: thesis: for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds
p `2 < 0

hence for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds
p `2 < 0 by A1, A3, JGRAPH_4:138; :: thesis: verum

end;

end;

end;

hence for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds
p `2 < 0 ; :: thesis: verum