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

now

per cases by A3, A5, Th74;

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

A27: (p2 `2 ) ^2 >= 0 by XREAL_1:65;
then A28: sqrt (1 + ((p2 `2 ) ^2 )) > 0 by SQUARE_1:93;
A29: p2 `1 = - 1 by A26, Th9;
A30: - 1 <= p2 `2 by A26, Th9;
A31: p2 `2 <= - (p2 `1 ) by A26, A29, Th9;
p2 <> 0. (TOP-REAL 2) by A29, EUCLID:56, EUCLID:58;
then A32: f . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (p2 `1 )) ^2 ))))]| by A2, A29, A30, A31, JGRAPH_3:def 1;
then A33: (f . p2) `1 = (p2 `1 ) / (sqrt (1 + (((p2 `2 ) / (- 1)) ^2 ))) by A29, EUCLID:56
.= (p2 `1 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) ;
A34: (f . p2) `2 = (p2 `2 ) / (sqrt (1 + (((p2 `2 ) / (- 1)) ^2 ))) by A29, A32, EUCLID:56
.= (p2 `2 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) ;
A35: (f . p2) `1 < 0 by A27, A29, A33, SQUARE_1:93, XREAL_1:143;
(p1 `2 ) * (sqrt (1 + ((p2 `2 ) ^2 ))) <= (p2 `2 ) * (sqrt (1 + ((p1 `2 ) ^2 ))) by A4, A26, 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 A28, XREAL_1:74;
then p1 `2 <= ((p2 `2 ) * (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p2 `2 ) ^2 ))) by A28, 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 A18, 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 A18, A22, A34, XCMPLX_1:90;
hence LE f . p1,f . p2,P by A7, A14, A15, A23, A24, A35, JGRAPH_5:56; :: thesis:

end;

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

then A37: p2 `2 = 1 by Th11;
A38: - 1 <= p2 `1 by A36, Th11;
A39: p2 `1 <= 1 by A36, Th11;
(p2 `1 ) ^2 >= 0 by XREAL_1:65;
then A40: sqrt (1 + ((p2 `1 ) ^2 )) > 0 by SQUARE_1:93;
p2 <> 0. (TOP-REAL 2) by A37, EUCLID:56, EUCLID:58;
then A41: f . p2 = |[((p2 `1 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 )))),((p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (p2 `2 )) ^2 ))))]| by A2, A37, A38, A39, JGRAPH_3:14;
then A42: (f . p2) `1 = (p2 `1 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) by A37, EUCLID:56;
A43: (f . p2) `2 >= 0 by A37, A40, A41, EUCLID:56;
- (sqrt (1 + ((p2 `1 ) ^2 ))) <= (p2 `1 ) * (sqrt (1 + ((p1 `2 ) ^2 ))) by A4, A9, A38, A39, 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 A8, A40, XREAL_1:74;
then p1 `1 <= ((p2 `1 ) * (sqrt (1 + ((p1 `2 ) ^2 )))) / (sqrt (1 + ((p2 `1 ) ^2 ))) by A40, 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 A18, 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 A18, A21, A42, XCMPLX_1:90;
hence LE f . p1,f . p2,P by A4, A7, A14, A15, A18, A22, A43, JGRAPH_5:57; :: thesis:

end;

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

then A45: p2 `1 = 1 by Th9;
A46: - 1 <= p2 `2 by A44, Th9;
A47: p2 `2 <= 1 by A44, Th9;
(p2 `2 ) ^2 >= 0 by XREAL_1:65;
then A48: sqrt (1 + ((p2 `2 ) ^2 )) > 0 by SQUARE_1:93;
p2 <> 0. (TOP-REAL 2) by A45, 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 A2, A45, A46, A47, JGRAPH_3:def 1;
then A49: (f . p2) `1 = (p2 `1 ) / (sqrt (1 + ((p2 `2 ) ^2 ))) by A45, EUCLID:56;
(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 A8, A18, A45, A48, 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 A50: (f . p1) `1 <= (f . p2) `1 by A18, A21, A49, 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 A4, A7, A14, A15, A18, A22, A50, JGRAPH_5:57; :: thesis:

end;

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

end;

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

end;

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

then A54: p2 `2 = - 1 by Th11;
A55: - 1 <= p2 `1 by A53, Th11;
A56: (p2 `1 ) ^2 >= 0 by XREAL_1:65;
A57: p2 `1 <= - (p2 `2 ) by A53, A54, Th11;
p2 <> 0. (TOP-REAL 2) by A54, 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 A2, A54, A55, A57, JGRAPH_3:14;
then (f . p2) `2 = (p2 `2 ) / (sqrt (1 + (((p2 `1 ) / (- 1)) ^2 ))) by A54, EUCLID:56
.= (p2 `2 ) / (sqrt (1 + ((p2 `1 ) ^2 ))) ;
then A58: (f . p2) `2 < 0 by A54, A56, SQUARE_1:93, XREAL_1:143;
then f . p2 in { p9 where p9 is Point of (TOP-REAL 2) : ( p9 in P & p9 `2 <= 0 ) } by A15;
then A59: f . p2 in Lower_Arc P by A7, JGRAPH_5:38;
W-min P = |[(- 1),0 ]| by A7, JGRAPH_5:32;
then f . p2 <> W-min P by A58, EUCLID:56;
hence LE f . p1,f . p2,P by A25, A59, JORDAN6:def 10; :: thesis:

end;

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