let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: for P being non empty compact Subset of (TOP-REAL 2)
for f being Function of (TOP-REAL 2),(TOP-REAL 2) st P = circle 0 ,0 ,1 & f = Sq_Circ & p1 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & p1 `2 >= 0 & LE p1,p2, rectangle (- 1),1,(- 1),1 & LE p2,p3, rectangle (- 1),1,(- 1),1 holds
LE f . p2,f . p3,P
let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for f being Function of (TOP-REAL 2),(TOP-REAL 2) st P = circle 0 ,0 ,1 & f = Sq_Circ & p1 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & p1 `2 >= 0 & LE p1,p2, rectangle (- 1),1,(- 1),1 & LE p2,p3, rectangle (- 1),1,(- 1),1 holds
LE f . p2,f . p3,P
let f be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: ( P = circle 0 ,0 ,1 & f = Sq_Circ & p1 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & p1 `2 >= 0 & LE p1,p2, rectangle (- 1),1,(- 1),1 & LE p2,p3, rectangle (- 1),1,(- 1),1 implies LE f . p2,f . p3,P )
set K = rectangle (- 1),1,(- 1),1;
assume that
A1: P = circle 0 ,0 ,1 and
A2: f = Sq_Circ and
A3: p1 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| and
A4: p1 `2 >= 0 and
A5: LE p1,p2, rectangle (- 1),1,(- 1),1 and
A6: LE p2,p3, rectangle (- 1),1,(- 1),1 ; :: thesis: LE f . p2,f . p3,P
A7: rectangle (- 1),1,(- 1),1 is being_simple_closed_curve by Th60;
A8: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } by A1, Th33;
A9: p3 in rectangle (- 1),1,(- 1),1 by A6, A7, JORDAN7:5;
A10: p2 in rectangle (- 1),1,(- 1),1 by A5, A7, JORDAN7:5;
A11: f .: (rectangle (- 1),1,(- 1),1) = P by A2, A8, Lm15, Th45, JGRAPH_3:33;
A12: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A13: f . p2 in P by A10, A11, FUNCT_1:def 12;
A14: f . p3 in P by A9, A11, A12, FUNCT_1:def 12;

now

per cases ( ( p2 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & p2 `2 >= p1 `2 ) or p2 in LSeg |[(- 1),1]|,|[1,1]| or p2 in LSeg |[1,1]|,|[1,(- 1)]| or ( p2 in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| & p2 <> |[(- 1),(- 1)]| ) ) by A3, A5, Th74;

case ( p2 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & p2 `2 >= p1 `2 ) ; :: thesis: LE f . p2,f . p3,P

hence LE f . p2,f . p3,P by A1, A2, A4, A6, Th75; :: thesis: verum

end;

case A15: p2 in LSeg |[(- 1),1]|,|[1,1]| ; :: thesis: LE f . p2,f . p3,P

then A16: p2 `2 = 1 by Th11;
A17: - 1 <= p2 `1 by A15, Th11;
A18: p2 `1 <= 1 by A15, Th11;
(p2 `1 ) ^2 >= 0 by XREAL_1:65;
then A19: sqrt (1 + ((p2 `1 ) ^2 )) > 0 by SQUARE_1:93;
p2 <> 0. (TOP-REAL 2) by A16, EUCLID:56, EUCLID:58;
then A20: f . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| by A2, A16, A17, A18, JGRAPH_3:14;
then A21: (f . p2) `1 = (p2 `1 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) by A16, EUCLID:56;
A22: (f . p2) `2 >= 0 by A16, A19, A20, EUCLID:56;
then f . p2 in { p9 where p9 is Point of (TOP-REAL 2) : ( p9 in P & p9 `2 >= 0 ) } by A13;
then A23: f . p2 in Upper_Arc P by A8, JGRAPH_5:37;

now

per cases ( ( p3 in LSeg |[(- 1),1]|,|[1,1]| & p2 `1 <= p3 `1 ) or p3 in LSeg |[1,1]|,|[1,(- 1)]| or ( p3 in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| & p3 <> W-min (rectangle (- 1),1,(- 1),1) ) ) by A6, A15, Th70;

case A24: ( p3 in LSeg |[(- 1),1]|,|[1,1]| & p2 `1 <= p3 `1 ) ; :: thesis: LE f . p2,f . p3,P

then A25: p3 `2 = 1 by Th11;
A26: - 1 <= p3 `1 by A24, Th11;
A27: p3 `1 <= 1 by A24, Th11;
(p3 `1 ) ^2 >= 0 by XREAL_1:65;
then A28: sqrt (1 + ((p3 `1 ) ^2 )) > 0 by SQUARE_1:93;
p3 <> 0. (TOP-REAL 2) by A25, EUCLID:56, EUCLID:58;
then A29: f . p3 = |[((p3 `1 ) / (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )))),((p3 `2 ) / (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))))]| by A2, A25, A26, A27, JGRAPH_3:14;
then A30: (f . p3) `1 = (p3 `1 ) / (sqrt (1 + ((p3 `1 ) ^2 ))) by A25, EUCLID:56;
A31: (f . p3) `2 >= 0 by A25, A28, A29, EUCLID:56;
(p2 `1 ) * (sqrt (1 + ((p3 `1 ) ^2 ))) <= (p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 ))) by A24, SQUARE_1:127;
then ((p2 `1 ) * (sqrt (1 + ((p3 `1 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 ))) <= ((p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 ))) by A28, XREAL_1:74;
then p2 `1 <= ((p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 ))) by A28, XCMPLX_1:90;
then (p2 `1 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) <= (((p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 )))) / (sqrt (1 + ((p2 `1 ) ^2 ))) by A19, XREAL_1:74;
then (p2 `1 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) <= (((p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 ))) by XCMPLX_1:48;
then (f . p2) `1 <= (f . p3) `1 by A19, A21, A30, XCMPLX_1:90;
hence LE f . p2,f . p3,P by A8, A13, A14, A22, A31, JGRAPH_5:57; :: thesis: verum

end;

case A32: p3 in LSeg |[1,1]|,|[1,(- 1)]| ; :: thesis: LE f . p2,f . p3,P

then A33: p3 `1 = 1 by Th9;
A34: - 1 <= p3 `2 by A32, Th9;
A35: p3 `2 <= 1 by A32, Th9;
(p3 `2 ) ^2 >= 0 by XREAL_1:65;
then A36: sqrt (1 + ((p3 `2 ) ^2 )) > 0 by SQUARE_1:93;
p3 <> 0. (TOP-REAL 2) by A33, EUCLID:56, EUCLID:58;
then f . p3 = |[((p3 `1 ) / (sqrt (1 + (((p3 `2 ) / (p3 `1 )) ^2 )))),((p3 `2 ) / (sqrt (1 + (((p3 `2 ) / (p3 `1 )) ^2 ))))]| by A2, A33, A34, A35, JGRAPH_3:def 1;
then A37: (f . p3) `1 = (p3 `1 ) / (sqrt (1 + ((p3 `2 ) ^2 ))) by A33, EUCLID:56;
A38: - 1 <= - (p2 `1 ) by A18, XREAL_1:26;
A39: - (- 1) >= - (p2 `1 ) by A17, XREAL_1:26;
(p2 `1 ) ^2 = (- (p2 `1 )) ^2 ;
then (- (- (p2 `1 ))) * (sqrt (1 + ((p3 `2 ) ^2 ))) <= sqrt (1 + ((p2 `1 ) ^2 )) by A34, A35, A38, A39, SQUARE_1:125;
then ((p2 `1 ) * (sqrt (1 + ((p3 `2 ) ^2 )))) / (sqrt (1 + ((p3 `2 ) ^2 ))) <= ((p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p3 `2 ) ^2 ))) by A33, A36, XREAL_1:74;
then p2 `1 <= ((p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p3 `2 ) ^2 ))) by A36, XCMPLX_1:90;
then (p2 `1 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) <= (((p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p3 `2 ) ^2 )))) / (sqrt (1 + ((p2 `1 ) ^2 ))) by A19, XREAL_1:74;
then (p2 `1 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) <= (((p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p3 `2 ) ^2 ))) by XCMPLX_1:48;
then A40: (f . p2) `1 <= (f . p3) `1 by A19, A21, A37, XCMPLX_1:90;

now

per cases ( (f . p3) `2 >= 0 or (f . p3) `2 < 0 ) ;

case (f . p3) `2 >= 0 ; :: thesis: LE f . p2,f . p3,P

hence LE f . p2,f . p3,P by A8, A13, A14, A22, A40, JGRAPH_5:57; :: thesis: verum

end;

case A41: (f . p3) `2 < 0 ; :: thesis: LE f . p2,f . p3,P

then f . p3 in { p9 where p9 is Point of (TOP-REAL 2) : ( p9 in P & p9 `2 <= 0 ) } by A14;
then A42: f . p3 in Lower_Arc P by A8, JGRAPH_5:38;
W-min P = |[(- 1),0 ]| by A8, JGRAPH_5:32;
then f . p3 <> W-min P by A41, EUCLID:56;
hence LE f . p2,f . p3,P by A23, A42, JORDAN6:def 10; :: thesis: verum

end;

end;

end;

hence LE f . p2,f . p3,P ; :: thesis: verum

end;

case A43: ( p3 in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| & p3 <> W-min (rectangle (- 1),1,(- 1),1) ) ; :: thesis: LE f . p2,f . p3,P

then A44: p3 `2 = - 1 by Th11;
A45: - 1 <= p3 `1 by A43, Th11;
A46: (p3 `1 ) ^2 >= 0 by XREAL_1:65;
A47: - (p3 `2 ) >= p3 `1 by A43, A44, Th11;
p3 <> 0. (TOP-REAL 2) by A44, EUCLID:56, EUCLID:58;
then f . p3 = |[((p3 `1 ) / (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )))),((p3 `2 ) / (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))))]| by A2, A44, A45, A47, JGRAPH_3:14;
then (f . p3) `2 = (p3 `2 ) / (sqrt (1 + (((p3 `1 ) / (- 1)) ^2 ))) by A44, EUCLID:56
.= (p3 `2 ) / (sqrt (1 + ((p3 `1 ) ^2 ))) ;
then A48: (f . p3) `2 < 0 by A44, A46, SQUARE_1:93, XREAL_1:143;
then f . p3 in { p9 where p9 is Point of (TOP-REAL 2) : ( p9 in P & p9 `2 <= 0 ) } by A14;
then A49: f . p3 in Lower_Arc P by A8, JGRAPH_5:38;
W-min P = |[(- 1),0 ]| by A8, JGRAPH_5:32;
then f . p3 <> W-min P by A48, EUCLID:56;
hence LE f . p2,f . p3,P by A23, A49, JORDAN6:def 10; :: thesis: verum

end;

end;

end;

hence LE f . p2,f . p3,P ; :: thesis: verum

end;

case A50: p2 in LSeg |[1,1]|,|[1,(- 1)]| ; :: thesis: LE f . p2,f . p3,P

then A51: p2 `1 = 1 by Th9;
A52: - 1 <= p2 `2 by A50, Th9;
A53: p2 `2 <= 1 by A50, Th9;
(p2 `2 ) ^2 >= 0 by XREAL_1:65;
then A54: sqrt (1 + ((p2 `2 ) ^2 )) > 0 by SQUARE_1:93;
p2 <> 0. (TOP-REAL 2) by A51, EUCLID:56, EUCLID:58;
then A55: f . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by A2, A51, A52, A53, JGRAPH_3:def 1;
then A56: (f . p2) `1 = (p2 `1 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) by A51, EUCLID:56;
A57: (f . p2) `2 = (p2 `2 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) by A51, A55, EUCLID:56;

now

per cases ( ( p3 in LSeg |[1,1]|,|[1,(- 1)]| & p2 `2 >= p3 `2 ) or ( p3 in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| & p3 <> W-min (rectangle (- 1),1,(- 1),1) ) ) by A6, A50, Th71;

case A58: ( p3 in LSeg |[1,1]|,|[1,(- 1)]| & p2 `2 >= p3 `2 ) ; :: thesis: LE f . p2,f . p3,P

then A59: p3 `1 = 1 by Th9;
A60: - 1 <= p3 `2 by A58, Th9;
A61: p3 `2 <= 1 by A58, Th9;
(p3 `2 ) ^2 >= 0 by XREAL_1:65;
then A62: sqrt (1 + ((p3 `2 ) ^2 )) > 0 by SQUARE_1:93;
p3 <> 0. (TOP-REAL 2) by A59, EUCLID:56, EUCLID:58;
then A63: f . p3 = |[((p3 `1 ) / (sqrt (1 + (((p3 `2 ) / (p3 `1 )) ^2 )))),((p3 `2 ) / (sqrt (1 + (((p3 `2 ) / (p3 `1 )) ^2 ))))]| by A2, A59, A60, A61, JGRAPH_3:def 1;
then A64: (f . p3) `2 = (p3 `2 ) / (sqrt (1 + ((p3 `2 ) ^2 ))) by A59, EUCLID:56;
A65: (f . p3) `1 >= 0 by A59, A62, A63, EUCLID:56;
(p2 `2 ) * (sqrt (1 + ((p3 `2 ) ^2 ))) >= (p3 `2 ) * (sqrt (1 + ((p2 `2 ) ^2 ))) by A58, SQUARE_1:127;
then ((p2 `2 ) * (sqrt (1 + ((p3 `2 ) ^2 )))) / (sqrt (1 + ((p3 `2 ) ^2 ))) >= ((p3 `2 ) * (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p3 `2 ) ^2 ))) by A62, XREAL_1:74;
then p2 `2 >= ((p3 `2 ) * (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p3 `2 ) ^2 ))) by A62, XCMPLX_1:90;
then (p2 `2 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) >= (((p3 `2 ) * (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p3 `2 ) ^2 )))) / (sqrt (1 + ((p2 `2 ) ^2 ))) by A54, XREAL_1:74;
then (p2 `2 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) >= (((p3 `2 ) * (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p3 `2 ) ^2 ))) by XCMPLX_1:48;
then (p2 `2 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) >= (p3 `2 ) / (sqrt (1 + ((p3 `2 ) ^2 ))) by A54, XCMPLX_1:90;
hence LE f . p2,f . p3,P by A8, A13, A14, A51, A54, A56, A57, A64, A65, JGRAPH_5:58; :: thesis: verum

end;

case A66: ( p3 in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| & p3 <> W-min (rectangle (- 1),1,(- 1),1) ) ; :: thesis: LE f . p2,f . p3,P

then A67: p3 `2 = - 1 by Th11;
A68: - 1 <= p3 `1 by A66, Th11;
A69: p3 `1 <= 1 by A66, Th11;
A70: (p3 `1 ) ^2 >= 0 by XREAL_1:65;
then A71: sqrt (1 + ((p3 `1 ) ^2 )) > 0 by SQUARE_1:93;
A72: - (p3 `2 ) >= p3 `1 by A66, A67, Th11;
p3 <> 0. (TOP-REAL 2) by A67, EUCLID:56, EUCLID:58;
then A73: f . p3 = |[((p3 `1 ) / (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )))),((p3 `2 ) / (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))))]| by A2, A67, A68, A72, JGRAPH_3:14;
then A74: (f . p3) `1 = (p3 `1 ) / (sqrt (1 + (((p3 `1 ) / (- 1)) ^2 ))) by A67, EUCLID:56
.= (p3 `1 ) / (sqrt (1 + ((p3 `1 ) ^2 ))) ;
A75: (f . p3) `2 = (p3 `2 ) / (sqrt (1 + (((p3 `1 ) / (- 1)) ^2 ))) by A67, A73, EUCLID:56
.= (p3 `2 ) / (sqrt (1 + ((p3 `1 ) ^2 ))) ;
then A76: (f . p3) `2 < 0 by A67, A70, SQUARE_1:93, XREAL_1:143;
f . p3 in { p9 where p9 is Point of (TOP-REAL 2) : ( p9 in P & p9 `2 <= 0 ) } by A14, A67, A71, A75;
then A77: f . p3 in Lower_Arc P by A8, JGRAPH_5:38;
W-min P = |[(- 1),0 ]| by A8, JGRAPH_5:32;
then A78: f . p3 <> W-min P by A76, EUCLID:56;

now

per cases ( (f . p2) `2 >= 0 or (f . p2) `2 < 0 ) ;

case (f . p2) `2 >= 0 ; :: thesis: LE f . p2,f . p3,P

then f . p2 in { p9 where p9 is Point of (TOP-REAL 2) : ( p9 in P & p9 `2 >= 0 ) } by A13;
then f . p2 in Upper_Arc P by A8, JGRAPH_5:37;
hence LE f . p2,f . p3,P by A77, A78, JORDAN6:def 10; :: thesis: verum

end;

case A79: (f . p2) `2 < 0 ; :: thesis: LE f . p2,f . p3,P

((p2 `1 ) * (sqrt (1 + ((p3 `1 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 ))) >= ((p3 `1 ) * (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 ))) by A51, A52, A53, A68, A69, A71, SQUARE_1:126, XREAL_1:74;
then p2 `1 >= ((p3 `1 ) * (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 ))) by A71, XCMPLX_1:90;
then (p2 `1 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) >= (((p3 `1 ) * (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 )))) / (sqrt (1 + ((p2 `2 ) ^2 ))) by A54, XREAL_1:74;
then (p2 `1 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) >= (((p3 `1 ) * (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 ))) by XCMPLX_1:48;
then (p2 `1 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) >= (p3 `1 ) / (sqrt (1 + ((p3 `1 ) ^2 ))) by A54, XCMPLX_1:90;
hence LE f . p2,f . p3,P by A8, A13, A14, A56, A67, A71, A74, A75, A78, A79, JGRAPH_5:59; :: thesis: verum

end;

end;

end;

hence LE f . p2,f . p3,P ; :: thesis: verum

end;

end;

end;

hence LE f . p2,f . p3,P ; :: thesis: verum

end;

case A80: ( p2 in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| & p2 <> |[(- 1),(- 1)]| ) ; :: thesis: LE f . p2,f . p3,P

then A81: p2 `2 = - 1 by Th11;
A82: - 1 <= p2 `1 by A80, Th11;
(p2 `1 ) ^2 >= 0 by XREAL_1:65;
then A83: sqrt (1 + ((p2 `1 ) ^2 )) > 0 by SQUARE_1:93;
A84: - (p2 `2 ) >= p2 `1 by A80, A81, Th11;
p2 <> 0. (TOP-REAL 2) by A81, EUCLID:56, EUCLID:58;
then A85: f . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| by A2, A81, A82, A84, JGRAPH_3:14;
then A86: (f . p2) `1 = (p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (- 1)) ^2 ))) by A81, EUCLID:56
.= (p2 `1 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) ;
A87: (f . p2) `2 = (p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (- 1)) ^2 ))) by A81, A85, EUCLID:56
.= (p2 `2 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) ;
A88: W-min (rectangle (- 1),1,(- 1),1) = |[(- 1),(- 1)]| by Th56;
then A89: p3 in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| by A6, A80, Th72;
A90: p2 `1 >= p3 `1 by A6, A80, A88, Th72;
A91: p3 `2 = - 1 by A89, Th11;
A92: - 1 <= p3 `1 by A89, Th11;
A93: (p3 `1 ) ^2 >= 0 by XREAL_1:65;
then A94: sqrt (1 + ((p3 `1 ) ^2 )) > 0 by SQUARE_1:93;
A95: - (p3 `2 ) >= p3 `1 by A89, A91, Th11;
p3 <> 0. (TOP-REAL 2) by A91, EUCLID:56, EUCLID:58;
then A96: f . p3 = |[((p3 `1 ) / (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )))),((p3 `2 ) / (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))))]| by A2, A91, A92, A95, JGRAPH_3:14;
then A97: (f . p3) `1 = (p3 `1 ) / (sqrt (1 + (((p3 `1 ) / (- 1)) ^2 ))) by A91, EUCLID:56
.= (p3 `1 ) / (sqrt (1 + ((p3 `1 ) ^2 ))) ;
(f . p3) `2 = (p3 `2 ) / (sqrt (1 + (((p3 `1 ) / (- 1)) ^2 ))) by A91, A96, EUCLID:56
.= (p3 `2 ) / (sqrt (1 + ((p3 `1 ) ^2 ))) ;
then A98: (f . p3) `2 < 0 by A91, A93, SQUARE_1:93, XREAL_1:143;
W-min P = |[(- 1),0 ]| by A8, JGRAPH_5:32;
then A99: f . p3 <> W-min P by A98, EUCLID:56;
(p2 `1 ) * (sqrt (1 + ((p3 `1 ) ^2 ))) >= (p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 ))) by A90, SQUARE_1:127;
then ((p2 `1 ) * (sqrt (1 + ((p3 `1 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 ))) >= ((p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 ))) by A94, XREAL_1:74;
then p2 `1 >= ((p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 ))) by A94, XCMPLX_1:90;
then (p2 `1 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) >= (((p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 )))) / (sqrt (1 + ((p2 `1 ) ^2 ))) by A83, XREAL_1:74;
then (p2 `1 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) >= (((p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 ))) by XCMPLX_1:48;
then (p2 `1 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) >= (p3 `1 ) / (sqrt (1 + ((p3 `1 ) ^2 ))) by A83, XCMPLX_1:90;
hence LE f . p2,f . p3,P by A8, A13, A14, A81, A83, A86, A87, A97, A98, A99, JGRAPH_5:59; :: thesis: verum

end;

end;

end;

hence LE f . p2,f . p3,P ; :: thesis: verum