let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis:
let P be non empty compact Subset of (TOP-REAL 2); :: thesis:
let f be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis:
set K = rectangle (- 1),1,(- 1),1;
assume A1: ( 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 ) ; :: thesis:
A2: rectangle (- 1),1,(- 1),1 is being_simple_closed_curve by Th60;
A3: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } by A1, Th33;
A4: p3 in rectangle (- 1),1,(- 1),1 by A1, A2, JORDAN7:5;
A5: p2 in rectangle (- 1),1,(- 1),1 by A1, A2, JORDAN7:5;
A6: f .: (rectangle (- 1),1,(- 1),1) = P by A1, A3, Lm8, Th45, JGRAPH_3:33;
A7: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A8: f . p2 in P by A5, A6, FUNCT_1:def 12;
A9: f . p3 in P by A4, A6, A7, FUNCT_1:def 12;

now

per cases by A1, Th74;

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

hence LE f . p2,f . p3,P by A1, Th75; :: thesis:

end;

case A10: p2 in LSeg |[(- 1),1]|,|[1,1]| ; :: thesis:

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

now

per cases by A1, A10, Th70;

case A18: ( p3 in LSeg |[(- 1),1]|,|[1,1]| & p2 `1 <= p3 `1 ) ; :: thesis:

then A19: ( p3 `2 = 1 & - 1 <= p3 `1 & p3 `1 <= 1 ) by Th11;
A20: (p3 `1 ) ^2 >= 0 by XREAL_1:65;
A21: sqrt (1 + ((p3 `1 ) ^2 )) > 0 by A20, SQUARE_1:93;
p3 <> 0.REAL 2 by A19, EUCLID:56, EUCLID:58;
then A22: f . p3 = |[((p3 `1 ) / (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )))),((p3 `2 ) / (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))))]| by A1, A19, JGRAPH_3:14;
then A23: (f . p3) `1 = (p3 `1 ) / (sqrt (1 + ((p3 `1 ) ^2 ))) by A19, EUCLID:56;
(f . p3) `2 = (p3 `2 ) / (sqrt (1 + ((p3 `1 ) ^2 ))) by A19, A22, EUCLID:56;
then A24: (f . p3) `2 >= 0 by A19, A21;
(p2 `1 ) * (sqrt (1 + ((p3 `1 ) ^2 ))) <= (p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 ))) by A18, 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 A21, XREAL_1:74;
then p2 `1 <= ((p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 ))) by A21, 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 A13, 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 A13, A15, A23, XCMPLX_1:90;
hence LE f . p2,f . p3,P by A3, A8, A9, A16, A24, JGRAPH_5:57; :: thesis:

end;

case p3 in LSeg |[1,1]|,|[1,(- 1)]| ; :: thesis:

then A25: ( p3 `1 = 1 & - 1 <= p3 `2 & p3 `2 <= 1 ) by Th9;
A26: (p3 `2 ) ^2 >= 0 by XREAL_1:65;
A27: sqrt (1 + ((p3 `2 ) ^2 )) > 0 by A26, SQUARE_1:93;
p3 <> 0.REAL 2 by A25, 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 A1, A25, JGRAPH_3:def 1;
then A28: (f . p3) `1 = (p3 `1 ) / (sqrt (1 + ((p3 `2 ) ^2 ))) by A25, EUCLID:56;
A29: - 1 <= - (p2 `1 ) by A11, XREAL_1:26;
A30: - (- 1) >= - (p2 `1 ) by A11, XREAL_1:26;
(p2 `1 ) ^2 = (- (p2 `1 )) ^2 ;
then (- (- (p2 `1 ))) * (sqrt (1 + ((p3 `2 ) ^2 ))) <= sqrt (1 + ((p2 `1 ) ^2 )) by A25, A29, A30, 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 A25, A27, XREAL_1:74;
then p2 `1 <= ((p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p3 `2 ) ^2 ))) by A27, 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 A13, 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 A31: (f . p2) `1 <= (f . p3) `1 by A13, A15, A28, XCMPLX_1:90;

now

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

case (f . p3) `2 >= 0 ; :: thesis:

hence LE f . p2,f . p3,P by A3, A8, A9, A16, A31, JGRAPH_5:57; :: thesis:

end;

case A32: (f . p3) `2 < 0 ; :: thesis:

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

end;

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

end;

case ( p3 in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| & p3 <> W-min (rectangle (- 1),1,(- 1),1) ) ; :: thesis:

then A34: ( p3 `2 = - 1 & - 1 <= p3 `1 & p3 `1 <= 1 ) by Th11;
A35: (p3 `1 ) ^2 >= 0 by XREAL_1:65;
A36: sqrt (1 + ((p3 `1 ) ^2 )) > 0 by A35, SQUARE_1:93;
A37: - (p3 `2 ) >= p3 `1 by A34;
p3 <> 0.REAL 2 by A34, 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 A1, A34, A37, JGRAPH_3:14;
then (f . p3) `2 = (p3 `2 ) / (sqrt (1 + (((p3 `1 ) / (- 1)) ^2 ))) by A34, EUCLID:56
.= (p3 `2 ) / (sqrt (1 + ((p3 `1 ) ^2 ))) ;
then A38: (f . p3) `2 < 0 by A34, A36, XREAL_1:143;
then f . p3 in { p9 where p9 is Point of (TOP-REAL 2) : ( p9 in P & p9 `2 <= 0 ) } by A9;
then A39: f . p3 in Lower_Arc P by A3, JGRAPH_5:38;
W-min P = |[(- 1),0 ]| by A3, JGRAPH_5:32;
then f . p3 <> W-min P by A38, EUCLID:56;
hence LE f . p2,f . p3,P by A17, A39, JORDAN6:def 10; :: thesis:

end;

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

end;

case A40: p2 in LSeg |[1,1]|,|[1,(- 1)]| ; :: thesis:

then A41: ( p2 `1 = 1 & - 1 <= p2 `2 & p2 `2 <= 1 ) by Th9;
A42: (p2 `2 ) ^2 >= 0 by XREAL_1:65;
A43: sqrt (1 + ((p2 `2 ) ^2 )) > 0 by A42, SQUARE_1:93;
p2 <> 0.REAL 2 by A41, EUCLID:56, EUCLID:58;
then A44: f . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by A1, A41, JGRAPH_3:def 1;
then A45: (f . p2) `1 = (p2 `1 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) by A41, EUCLID:56;
A46: (f . p2) `2 = (p2 `2 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) by A41, A44, EUCLID:56;
A47: (f . p2) `1 >= 0 by A41, A43, A45;

now

per cases by A1, A40, Th71;

case A48: ( p3 in LSeg |[1,1]|,|[1,(- 1)]| & p2 `2 >= p3 `2 ) ; :: thesis:

then A49: ( p3 `1 = 1 & - 1 <= p3 `2 & p3 `2 <= 1 ) by Th9;
A50: (p3 `2 ) ^2 >= 0 by XREAL_1:65;
A51: sqrt (1 + ((p3 `2 ) ^2 )) > 0 by A50, SQUARE_1:93;
p3 <> 0.REAL 2 by A49, EUCLID:56, EUCLID:58;
then A52: f . p3 = |[((p3 `1 ) / (sqrt (1 + (((p3 `2 ) / (p3 `1 )) ^2 )))),((p3 `2 ) / (sqrt (1 + (((p3 `2 ) / (p3 `1 )) ^2 ))))]| by A1, A49, JGRAPH_3:def 1;
then A53: (f . p3) `1 = (p3 `1 ) / (sqrt (1 + ((p3 `2 ) ^2 ))) by A49, EUCLID:56;
A54: (f . p3) `2 = (p3 `2 ) / (sqrt (1 + ((p3 `2 ) ^2 ))) by A49, A52, EUCLID:56;
A55: (f . p3) `1 >= 0 by A49, A51, A53;
(p2 `2 ) * (sqrt (1 + ((p3 `2 ) ^2 ))) >= (p3 `2 ) * (sqrt (1 + ((p2 `2 ) ^2 ))) by A48, 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 A51, XREAL_1:74;
then p2 `2 >= ((p3 `2 ) * (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p3 `2 ) ^2 ))) by A51, 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 A43, 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 A43, XCMPLX_1:90;
hence LE f . p2,f . p3,P by A3, A8, A9, A46, A47, A54, A55, JGRAPH_5:58; :: thesis:

end;

case ( p3 in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| & p3 <> W-min (rectangle (- 1),1,(- 1),1) ) ; :: thesis:

then A56: ( p3 `2 = - 1 & - 1 <= p3 `1 & p3 `1 <= 1 ) by Th11;
A57: (p3 `1 ) ^2 >= 0 by XREAL_1:65;
A58: sqrt (1 + ((p3 `1 ) ^2 )) > 0 by A57, SQUARE_1:93;
A59: - (p3 `2 ) >= p3 `1 by A56;
p3 <> 0.REAL 2 by A56, EUCLID:56, EUCLID:58;
then A60: f . p3 = |[((p3 `1 ) / (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )))),((p3 `2 ) / (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))))]| by A1, A56, A59, JGRAPH_3:14;
then A61: (f . p3) `1 = (p3 `1 ) / (sqrt (1 + (((p3 `1 ) / (- 1)) ^2 ))) by A56, EUCLID:56
.= (p3 `1 ) / (sqrt (1 + ((p3 `1 ) ^2 ))) ;
(f . p3) `2 = (p3 `2 ) / (sqrt (1 + (((p3 `1 ) / (- 1)) ^2 ))) by A56, A60, EUCLID:56
.= (p3 `2 ) / (sqrt (1 + ((p3 `1 ) ^2 ))) ;
then A62: (f . p3) `2 < 0 by A56, A58, XREAL_1:143;
then f . p3 in { p9 where p9 is Point of (TOP-REAL 2) : ( p9 in P & p9 `2 <= 0 ) } by A9;
then A63: f . p3 in Lower_Arc P by A3, JGRAPH_5:38;
W-min P = |[(- 1),0 ]| by A3, JGRAPH_5:32;
then A64: f . p3 <> W-min P by A62, EUCLID:56;

now

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

case (f . p2) `2 >= 0 ; :: thesis:

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

end;

case A65: (f . p2) `2 < 0 ; :: thesis:

sqrt (1 + ((p3 `1 ) ^2 )) >= (p3 `1 ) * (sqrt (1 + ((p2 `2 ) ^2 ))) by A41, A56, SQUARE_1:126;
then ((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 A41, A58, XREAL_1:74;
then p2 `1 >= ((p3 `1 ) * (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 ))) by A58, 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 A43, 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 A43, XCMPLX_1:90;
hence LE f . p2,f . p3,P by A3, A8, A9, A45, A61, A62, A64, A65, JGRAPH_5:59; :: thesis:

end;

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

end;

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

end;

case A66: ( p2 in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| & p2 <> |[(- 1),(- 1)]| ) ; :: thesis:

then A67: ( p2 `2 = - 1 & - 1 <= p2 `1 & p2 `1 <= 1 ) by Th11;
A68: (p2 `1 ) ^2 >= 0 by XREAL_1:65;
A69: sqrt (1 + ((p2 `1 ) ^2 )) > 0 by A68, SQUARE_1:93;
A70: - (p2 `2 ) >= p2 `1 by A67;
p2 <> 0.REAL 2 by A67, EUCLID:56, EUCLID:58;
then A71: f . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| by A1, A67, A70, JGRAPH_3:14;
then A72: (f . p2) `1 = (p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (- 1)) ^2 ))) by A67, EUCLID:56
.= (p2 `1 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) ;
(f . p2) `2 = (p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (- 1)) ^2 ))) by A67, A71, EUCLID:56
.= (p2 `2 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) ;
then A73: (f . p2) `2 < 0 by A67, A69, XREAL_1:143;
W-min (rectangle (- 1),1,(- 1),1) = |[(- 1),(- 1)]| by Th56;
then A74: ( p3 in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| & p2 `1 >= p3 `1 & p3 <> W-min (rectangle (- 1),1,(- 1),1) ) by A1, A66, Th72;
then A75: ( p3 `2 = - 1 & - 1 <= p3 `1 & p3 `1 <= 1 ) by Th11;
A76: (p3 `1 ) ^2 >= 0 by XREAL_1:65;
A77: sqrt (1 + ((p3 `1 ) ^2 )) > 0 by A76, SQUARE_1:93;
A78: - (p3 `2 ) >= p3 `1 by A75;
p3 <> 0.REAL 2 by A75, EUCLID:56, EUCLID:58;
then A79: f . p3 = |[((p3 `1 ) / (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 )))),((p3 `2 ) / (sqrt (1 + (((p3 `1 ) / (p3 `2 )) ^2 ))))]| by A1, A75, A78, JGRAPH_3:14;
then A80: (f . p3) `1 = (p3 `1 ) / (sqrt (1 + (((p3 `1 ) / (- 1)) ^2 ))) by A75, EUCLID:56
.= (p3 `1 ) / (sqrt (1 + ((p3 `1 ) ^2 ))) ;
(f . p3) `2 = (p3 `2 ) / (sqrt (1 + (((p3 `1 ) / (- 1)) ^2 ))) by A75, A79, EUCLID:56
.= (p3 `2 ) / (sqrt (1 + ((p3 `1 ) ^2 ))) ;
then A81: (f . p3) `2 < 0 by A75, A77, XREAL_1:143;
W-min P = |[(- 1),0 ]| by A3, JGRAPH_5:32;
then A82: f . p3 <> W-min P by A81, EUCLID:56;
(p2 `1 ) * (sqrt (1 + ((p3 `1 ) ^2 ))) >= (p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 ))) by A74, 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 A77, XREAL_1:74;
then p2 `1 >= ((p3 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p3 `1 ) ^2 ))) by A77, 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 A69, 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 A69, XCMPLX_1:90;
hence LE f . p2,f . p3,P by A3, A8, A9, A72, A73, A80, A81, A82, JGRAPH_5:59; :: thesis:

end;

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