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

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

per cases ( (q `2) / |.q.| >= sn or (q `2) / |.q.| < sn ) ;

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

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

end;

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

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

end;

end;

end;

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