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 Th50;
A7: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } by A1, Th24;
A8: p1 `1 = - 1 by A3, Th1;
A9: p1 `2 <= 1 by A3, Th1;
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, Th35, JGRAPH_3:23;
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 6;
A15: f . p2 in P by A11, A12, A13, FUNCT_1:def 6;
A16: p1 `1 = - 1 by A3, Th1;
A17: (p1 `2) ^2 >= 0 by XREAL_1:63;
then A18: sqrt (1 + ((p1 `2) ^2)) > 0 by SQUARE_1:25;
A19: p1 `2 <= - (p1 `1) by A3, A8, Th1;
p1 <> 0. (TOP-REAL 2) by A8, EUCLID:52, EUCLID:54;
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:52
.= (p1 `1) / (sqrt (1 + ((p1 `2) ^2))) ;
A22: (f . p1) `2 = (p1 `2) / (sqrt (1 + (((p1 `2) / (- 1)) ^2))) by A16, A20, EUCLID:52
.= (p1 `2) / (sqrt (1 + ((p1 `2) ^2))) ;
A23: (f . p1) `1 < 0 by A16, A17, A21, SQUARE_1:25, XREAL_1:141;
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:34;

now :: thesis:

per cases by A3, A5, Th64;

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

A27: (p2 `2) ^2 >= 0 by XREAL_1:63;
then A28: sqrt (1 + ((p2 `2) ^2)) > 0 by SQUARE_1:25;
A29: p2 `1 = - 1 by A26, Th1;
A30: - 1 <= p2 `2 by A26, Th1;
A31: p2 `2 <= - (p2 `1) by A26, A29, Th1;
p2 <> 0. (TOP-REAL 2) by A29, EUCLID:52, EUCLID:54;
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:52
.= (p2 `1) / (sqrt (1 + ((p2 `2) ^2))) ;
A34: (f . p2) `2 = (p2 `2) / (sqrt (1 + (((p2 `2) / (- 1)) ^2))) by A29, A32, EUCLID:52
.= (p2 `2) / (sqrt (1 + ((p2 `2) ^2))) ;
A35: (f . p2) `1 < 0 by A27, A29, A33, SQUARE_1:25, XREAL_1:141;
(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:72;
then p1 `2 <= ((p2 `2) * (sqrt (1 + ((p1 `2) ^2)))) / (sqrt (1 + ((p2 `2) ^2))) by A28, XCMPLX_1:89;
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:72;
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:89;
hence LE f . p1,f . p2,P by A7, A14, A15, A23, A24, A35, JGRAPH_5:53; :: thesis:

end;

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

then A37: p2 `2 = 1 by Th3;
A38: - 1 <= p2 `1 by A36, Th3;
A39: p2 `1 <= 1 by A36, Th3;
(p2 `1) ^2 >= 0 by XREAL_1:63;
then A40: sqrt (1 + ((p2 `1) ^2)) > 0 by SQUARE_1:25;
p2 <> 0. (TOP-REAL 2) by A37, EUCLID:52, EUCLID:54;
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:4;
then A42: (f . p2) `1 = (p2 `1) / (sqrt (1 + ((p2 `1) ^2))) by A37, EUCLID:52;
A43: (f . p2) `2 >= 0 by A37, A40, A41, EUCLID:52;
- (sqrt (1 + ((p2 `1) ^2))) <= (p2 `1) * (sqrt (1 + ((p1 `2) ^2))) by A4, A9, A38, A39, SQUARE_1:55;
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:72;
then p1 `1 <= ((p2 `1) * (sqrt (1 + ((p1 `2) ^2)))) / (sqrt (1 + ((p2 `1) ^2))) by A40, XCMPLX_1:89;
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:72;
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:89;
hence LE f . p1,f . p2,P by A4, A7, A14, A15, A18, A22, A43, JGRAPH_5:54; :: thesis:

end;

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

then A45: p2 `1 = 1 by Th1;
A46: - 1 <= p2 `2 by A44, Th1;
A47: p2 `2 <= 1 by A44, Th1;
(p2 `2) ^2 >= 0 by XREAL_1:63;
then A48: sqrt (1 + ((p2 `2) ^2)) > 0 by SQUARE_1:25;
p2 <> 0. (TOP-REAL 2) by A45, EUCLID:52, EUCLID:54;
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:52;
(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:72;
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:89;

now :: thesis:

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:54; :: 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:35;
W-min P = |[(- 1),0]| by A7, JGRAPH_5:29;
then f . p2 <> W-min P by A51, EUCLID:52;
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 Th3;
A55: - 1 <= p2 `1 by A53, Th3;
A56: (p2 `1) ^2 >= 0 by XREAL_1:63;
A57: p2 `1 <= - (p2 `2) by A53, A54, Th3;
p2 <> 0. (TOP-REAL 2) by A54, EUCLID:52, EUCLID:54;
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:4;
then (f . p2) `2 = (p2 `2) / (sqrt (1 + (((p2 `1) / (- 1)) ^2))) by A54, EUCLID:52
.= (p2 `2) / (sqrt (1 + ((p2 `1) ^2))) ;
then A58: (f . p2) `2 < 0 by A54, A56, SQUARE_1:25, XREAL_1:141;
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:35;
W-min P = |[(- 1),0]| by A7, JGRAPH_5:29;
then f . p2 <> W-min P by A58, EUCLID:52;
hence LE f . p1,f . p2,P by A25, A59, JORDAN6:def 10; :: thesis:

end;

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