let p1, p2 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 ) ; :: 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: ( p1 `1 = - 1 & - 1 <= p1 `2 & p1 `2 <= 1 ) by A1, Th9;
A5: p1 in rectangle (- 1),1,(- 1),1 by A1, A2, JORDAN7:5;
A6: p2 in rectangle (- 1),1,(- 1),1 by A1, A2, JORDAN7:5;
A7: f .: (rectangle (- 1),1,(- 1),1) = P by A1, A3, Lm8, Th45, JGRAPH_3:33;
A8: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A9: f . p1 in P by A5, A7, FUNCT_1:def 12;
A10: f . p2 in P by A6, A7, A8, FUNCT_1:def 12;
A11: ( p1 `1 = - 1 & - 1 <= p1 `2 & p1 `2 <= 1 ) by A1, Th9;
A12: (p1 `2 ) ^2 >= 0 by XREAL_1:65;
A13: sqrt (1 + ((p1 `2 ) ^2 )) > 0 by A12, SQUARE_1:93;
A14: p1 `2 <= - (p1 `1 ) by A4;
p1 <> 0. (TOP-REAL 2) by A4, EUCLID:56, EUCLID:58;
then A15: f . p1 = |[((p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 )))),((p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (p1 `1 )) ^2 ))))]| by A1, A11, A14, JGRAPH_3:def 1;
then A16: (f . p1) `1 = (p1 `1 ) / (sqrt (1 + (((p1 `2 ) / (- 1)) ^2 ))) by A11, EUCLID:56
.= (p1 `1 ) / (sqrt (1 + ((p1 `2 ) ^2 ))) ;
A17: (f . p1) `2 = (p1 `2 ) / (sqrt (1 + (((p1 `2 ) / (- 1)) ^2 ))) by A11, A15, EUCLID:56
.= (p1 `2 ) / (sqrt (1 + ((p1 `2 ) ^2 ))) ;
A18: (f . p1) `1 < 0 by A11, A13, A16, XREAL_1:143;
A19: (f . p1) `2 >= 0 by A1, A13, A17;
then f . p1 in { p9 where p9 is Point of (TOP-REAL 2) : ( p9 in P & p9 `2 >= 0 ) } by A9;
then A20: f . p1 in Upper_Arc P by A3, JGRAPH_5:37;

now

per cases by A1, Th74;

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

A22: (p2 `2 ) ^2 >= 0 by XREAL_1:65;
A23: sqrt (1 + ((p2 `2 ) ^2 )) > 0 by A22, SQUARE_1:93;
A24: ( p2 `1 = - 1 & - 1 <= p2 `2 & p2 `2 <= 1 ) by A21, Th9;
then A25: p2 `2 <= - (p2 `1 ) ;
p2 <> 0. (TOP-REAL 2) by A24, EUCLID:56, EUCLID:58;
then A26: f . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by A1, A24, A25, JGRAPH_3:def 1;
then A27: (f . p2) `1 = (p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (- 1)) ^2 ))) by A24, EUCLID:56
.= (p2 `1 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) ;
A28: (f . p2) `2 = (p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (- 1)) ^2 ))) by A24, A26, EUCLID:56
.= (p2 `2 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) ;
A29: (f . p2) `1 < 0 by A23, A24, A27, XREAL_1:143;
(p1 `2 ) * (sqrt (1 + ((p2 `2 ) ^2 ))) <= (p2 `2 ) * (sqrt (1 + ((p1 `2 ) ^2 ))) by A1, A21, Lm3;
then ((p1 `2 ) * (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p2 `2 ) ^2 ))) <= ((p2 `2 ) * (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p2 `2 ) ^2 ))) by A23, XREAL_1:74;
then p1 `2 <= ((p2 `2 ) * (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p2 `2 ) ^2 ))) by A23, XCMPLX_1:90;
then (p1 `2 ) / (sqrt (1 + ((p1 `2 ) ^2 ))) <= (((p2 `2 ) * (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p1 `2 ) ^2 ))) by A13, XREAL_1:74;
then (p1 `2 ) / (sqrt (1 + ((p1 `2 ) ^2 ))) <= (((p2 `2 ) * (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p2 `2 ) ^2 ))) by XCMPLX_1:48;
then (f . p1) `2 <= (f . p2) `2 by A13, A17, A28, XCMPLX_1:90;
hence LE f . p1,f . p2,P by A3, A9, A10, A18, A19, A29, JGRAPH_5:56; :: thesis:

end;

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

then A30: ( p2 `2 = 1 & - 1 <= p2 `1 & p2 `1 <= 1 ) by Th11;
A31: (p2 `1 ) ^2 >= 0 by XREAL_1:65;
A32: sqrt (1 + ((p2 `1 ) ^2 )) > 0 by A31, SQUARE_1:93;
p2 <> 0. (TOP-REAL 2) by A30, EUCLID:56, EUCLID:58;
then A33: f . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| by A1, A30, JGRAPH_3:14;
then A34: (f . p2) `1 = (p2 `1 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) by A30, EUCLID:56;
(f . p2) `2 = (p2 `2 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) by A30, A33, EUCLID:56;
then A35: (f . p2) `2 >= 0 by A30, A32;
- (sqrt (1 + ((p2 `1 ) ^2 ))) <= (p2 `1 ) * (sqrt (1 + ((p1 `2 ) ^2 ))) by A4, A30, SQUARE_1:125;
then ((p1 `1 ) * (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p2 `1 ) ^2 ))) <= ((p2 `1 ) * (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p2 `1 ) ^2 ))) by A4, A32, XREAL_1:74;
then p1 `1 <= ((p2 `1 ) * (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p2 `1 ) ^2 ))) by A32, XCMPLX_1:90;
then (p1 `1 ) / (sqrt (1 + ((p1 `2 ) ^2 ))) <= (((p2 `1 ) * (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p2 `1 ) ^2 )))) / (sqrt (1 + ((p1 `2 ) ^2 ))) by A13, XREAL_1:74;
then (p1 `1 ) / (sqrt (1 + ((p1 `2 ) ^2 ))) <= (((p2 `1 ) * (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p2 `1 ) ^2 ))) by XCMPLX_1:48;
then (f . p1) `1 <= (f . p2) `1 by A13, A16, A34, XCMPLX_1:90;
hence LE f . p1,f . p2,P by A3, A9, A10, A19, A35, JGRAPH_5:57; :: thesis:

end;

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

then A36: ( p2 `1 = 1 & - 1 <= p2 `2 & p2 `2 <= 1 ) by Th9;
A37: (p2 `2 ) ^2 >= 0 by XREAL_1:65;
A38: sqrt (1 + ((p2 `2 ) ^2 )) > 0 by A37, SQUARE_1:93;
p2 <> 0. (TOP-REAL 2) by A36, EUCLID:56, EUCLID:58;
then f . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by A1, A36, JGRAPH_3:def 1;
then A39: (f . p2) `1 = (p2 `1 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) by A36, EUCLID:56;
(p1 `1 ) * (sqrt (1 + ((p2 `2 ) ^2 ))) <= 0 by A4, A38;
then ((p1 `1 ) * (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p2 `2 ) ^2 ))) <= ((p2 `1 ) * (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p2 `2 ) ^2 ))) by A13, A36, A38, XREAL_1:76;
then p1 `1 <= ((p2 `1 ) * (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p2 `2 ) ^2 ))) by A38, XCMPLX_1:90;
then (p1 `1 ) / (sqrt (1 + ((p1 `2 ) ^2 ))) <= (((p2 `1 ) * (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p2 `2 ) ^2 )))) / (sqrt (1 + ((p1 `2 ) ^2 ))) by A13, XREAL_1:74;
then (p1 `1 ) / (sqrt (1 + ((p1 `2 ) ^2 ))) <= (((p2 `1 ) * (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p2 `2 ) ^2 ))) by XCMPLX_1:48;
then A40: (f . p1) `1 <= (f . p2) `1 by A13, A16, A39, XCMPLX_1:90;

now

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

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

hence LE f . p1,f . p2,P by A3, A9, A10, A19, A40, JGRAPH_5:57; :: thesis:

end;

case A41: (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 A10;
then A42: f . p2 in Lower_Arc P by A3, JGRAPH_5:38;
W-min P = |[(- 1),0 ]| by A3, JGRAPH_5:32;
then f . p2 <> W-min P by A41, EUCLID:56;
hence LE f . p1,f . p2,P by A20, A42, JORDAN6:def 10; :: thesis:

end;

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

end;

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

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

end;

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