let p be Point of (TOP-REAL 2); :: thesis: for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = Sq_Circ & p `1 = - 1 & p `2 < 0 holds
( (f . p) `1 < 0 & (f . p) `2 < 0 )
let f be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: ( f = Sq_Circ & p `1 = - 1 & p `2 < 0 implies ( (f . p) `1 < 0 & (f . p) `2 < 0 ) )
assume that
A1: f = Sq_Circ and
A2: p `1 = - 1 and
A3: p `2 < 0 ; :: thesis: ( (f . p) `1 < 0 & (f . p) `2 < 0 )

now :: thesis: ( ( p = 0. (TOP-REAL 2) & contradiction ) or ( p <> 0. (TOP-REAL 2) & (f . p) `1 < 0 & (f . p) `2 < 0 ) )

per cases ( p = 0. (TOP-REAL 2) or p <> 0. (TOP-REAL 2) ) ;

case p = 0. (TOP-REAL 2) ; :: thesis: contradiction

hence contradiction by A2, EUCLID:52, EUCLID:54; :: thesis: verum

end;

case A4: p <> 0. (TOP-REAL 2) ; :: thesis: ( (f . p) `1 < 0 & (f . p) `2 < 0 )

now :: thesis: ( ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & (f . p) `1 < 0 & (f . p) `2 < 0 ) or ( not ( p `2 <= p `1 & - (p `1) <= p `2 ) & not ( p `2 >= p `1 & p `2 <= - (p `1) ) & (f . p) `1 < 0 & (f . p) `2 < 0 ) )

per cases ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or ( not ( p `2 <= p `1 & - (p `1) <= p `2 ) & not ( p `2 >= p `1 & p `2 <= - (p `1) ) ) ) ;

case ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) ; :: thesis: ( (f . p) `1 < 0 & (f . p) `2 < 0 )

then A5: f . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| by A1, A4, JGRAPH_3:def 1;
then A6: (f . p) `1 = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) by EUCLID:52;
(f . p) `2 = (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) by A5, EUCLID:52;
hence ( (f . p) `1 < 0 & (f . p) `2 < 0 ) by A2, A3, A6, SQUARE_1:25, XREAL_1:141; :: thesis: verum

end;

case ( not ( p `2 <= p `1 & - (p `1) <= p `2 ) & not ( p `2 >= p `1 & p `2 <= - (p `1) ) ) ; :: thesis: ( (f . p) `1 < 0 & (f . p) `2 < 0 )

then A7: f . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| by A1, A4, JGRAPH_3:def 1;
then A8: (f . p) `1 = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) by EUCLID:52;
(f . p) `2 = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) by A7, EUCLID:52;
hence ( (f . p) `1 < 0 & (f . p) `2 < 0 ) by A2, A3, A8, SQUARE_1:25, XREAL_1:141; :: thesis: verum

end;

end;

end;

hence ( (f . p) `1 < 0 & (f . p) `2 < 0 ) ; :: thesis: verum

end;

end;

end;

hence ( (f . p) `1 < 0 & (f . p) `2 < 0 ) ; :: thesis: verum