let sn be Real; :: thesis: for q being Point of (TOP-REAL 2) st - 1 < sn & sn < 1 & q `1 >= 0 & (q `2) / |.q.| < sn & |.q.| <> 0 holds
for p being Point of (TOP-REAL 2) st p = (sn -FanMorphE) . q holds
( p `1 >= 0 & p `2 < 0 )
let q be Point of (TOP-REAL 2); :: thesis: ( - 1 < sn & sn < 1 & q `1 >= 0 & (q `2) / |.q.| < sn & |.q.| <> 0 implies for p being Point of (TOP-REAL 2) st p = (sn -FanMorphE) . q holds
( p `1 >= 0 & p `2 < 0 ) )
assume that
A1: - 1 < sn and
A2: sn < 1 and
A3: ( q `1 >= 0 & (q `2) / |.q.| < sn ) and
A4: |.q.| <> 0 ; :: thesis: for p being Point of (TOP-REAL 2) st p = (sn -FanMorphE) . q holds
( p `1 >= 0 & p `2 < 0 )
let p be Point of (TOP-REAL 2); :: thesis: ( p = (sn -FanMorphE) . q implies ( p `1 >= 0 & p `2 < 0 ) )
assume A5: p = (sn -FanMorphE) . q ; :: thesis: ( p `1 >= 0 & p `2 < 0 )

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

per cases ( q `1 = 0 or q `1 <> 0 ) ;

case A6: q `1 = 0 ; :: thesis: ( p `1 >= 0 & p `2 < 0 )

then |.q.| ^2 = ((q `2) ^2) + (0 ^2) by JGRAPH_3:1
.= (q `2) ^2 ;
then A7: ( |.q.| = q `2 or |.q.| = - (q `2) ) by SQUARE_1:40;
q = p by A5, A6, JGRAPH_4:82;
hence ( p `1 >= 0 & p `2 < 0 ) by A2, A3, A4, A7, XCMPLX_1:60; :: thesis: verum

end;

case q `1 <> 0 ; :: thesis: ( p `1 >= 0 & p `2 < 0 )

hence ( p `1 >= 0 & p `2 < 0 ) by A1, A3, A5, JGRAPH_4:107; :: thesis: verum

end;

end;

end;

hence ( p `1 >= 0 & p `2 < 0 ) ; :: thesis: verum