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

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

per cases ( q `2 > 0 or q `2 = 0 ) by A2;

case q `2 > 0 ; :: 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, Th18; :: thesis: verum

end;

case q `2 = 0 ; :: 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 JGRAPH_4:49; :: 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