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 -FanMorphN) . 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 -FanMorphN) . 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 -FanMorphN) . q holds
p `2 > 0

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

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

end;

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

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

end;

end;

end;

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