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 Th50;
A8: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } by A1, Th24;
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, Th35, JGRAPH_3:23;
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 6;
A14: f . p3 in P by A9, A11, A12, FUNCT_1:def 6;
now :: thesis: ( ( p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & p2 `2 >= p1 `2 & LE f . p2,f . p3,P ) or ( p2 in LSeg (|[(- 1),1]|,|[1,1]|) & LE f . p2,f . p3,P ) or ( p2 in LSeg (|[1,1]|,|[1,(- 1)]|) & LE f . p2,f . p3,P ) or ( p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p2 <> |[(- 1),(- 1)]| & LE f . p2,f . p3,P ) )
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, Th64;
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, Th65; :: 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 Th3;
A17: - 1 <= p2 `1 by A15, Th3;
A18: p2 `1 <= 1 by A15, Th3;
(p2 `1) ^2 >= 0 by XREAL_1:63;
then A19: sqrt (1 + ((p2 `1) ^2)) > 0 by SQUARE_1:25;
p2 <> 0. (TOP-REAL 2) by A16, EUCLID:52, EUCLID:54;
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:4;
then A21: (f . p2) `1 = (p2 `1) / (sqrt (1 + ((p2 `1) ^2))) by A16, EUCLID:52;
A22: (f . p2) `2 >= 0 by A16, A19, A20, EUCLID:52;
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:34;
now :: thesis: ( ( p3 in LSeg (|[(- 1),1]|,|[1,1]|) & p2 `1 <= p3 `1 & LE f . p2,f . p3,P ) or ( p3 in LSeg (|[1,1]|,|[1,(- 1)]|) & LE f . p2,f . p3,P ) or ( p3 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p3 <> W-min (rectangle ((- 1),1,(- 1),1)) & LE f . p2,f . p3,P ) )
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, Th60;
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 Th3;
A26: - 1 <= p3 `1 by A24, Th3;
A27: p3 `1 <= 1 by A24, Th3;
(p3 `1) ^2 >= 0 by XREAL_1:63;
then A28: sqrt (1 + ((p3 `1) ^2)) > 0 by SQUARE_1:25;
p3 <> 0. (TOP-REAL 2) by A25, EUCLID:52, EUCLID:54;
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:4;
then A30: (f . p3) `1 = (p3 `1) / (sqrt (1 + ((p3 `1) ^2))) by A25, EUCLID:52;
A31: (f . p3) `2 >= 0 by A25, A28, A29, EUCLID:52;
(p2 `1) * (sqrt (1 + ((p3 `1) ^2))) <= (p3 `1) * (sqrt (1 + ((p2 `1) ^2))) by A24, SQUARE_1:57;
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:72;
then p2 `1 <= ((p3 `1) * (sqrt (1 + ((p2 `1) ^2)))) / (sqrt (1 + ((p3 `1) ^2))) by A28, XCMPLX_1:89;
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:72;
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:89;
hence LE f . p2,f . p3,P by A8, A13, A14, A22, A31, JGRAPH_5:54; :: 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 Th1;
A34: - 1 <= p3 `2 by A32, Th1;
A35: p3 `2 <= 1 by A32, Th1;
(p3 `2) ^2 >= 0 by XREAL_1:63;
then A36: sqrt (1 + ((p3 `2) ^2)) > 0 by SQUARE_1:25;
p3 <> 0. (TOP-REAL 2) by A33, EUCLID:52, EUCLID:54;
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:52;
A38: - 1 <= - (p2 `1) by A18, XREAL_1:24;
A39: - (- 1) >= - (p2 `1) by A17, XREAL_1:24;
(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:55;
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:72;
then p2 `1 <= ((p3 `1) * (sqrt (1 + ((p2 `1) ^2)))) / (sqrt (1 + ((p3 `2) ^2))) by A36, XCMPLX_1:89;
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:72;
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:89;
now :: thesis: ( ( (f . p3) `2 >= 0 & LE f . p2,f . p3,P ) or ( (f . p3) `2 < 0 & LE f . p2,f . p3,P ) )
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:54; :: 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:35;
W-min P = |[(- 1),0]| by A8, JGRAPH_5:29;
then f . p3 <> W-min P by A41, EUCLID:52;
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 Th3;
A45: - 1 <= p3 `1 by A43, Th3;
A46: (p3 `1) ^2 >= 0 by XREAL_1:63;
A47: - (p3 `2) >= p3 `1 by A43, A44, Th3;
p3 <> 0. (TOP-REAL 2) by A44, EUCLID:52, EUCLID:54;
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:4;
then (f . p3) `2 = (p3 `2) / (sqrt (1 + (((p3 `1) / (- 1)) ^2))) by A44, EUCLID:52
.= (p3 `2) / (sqrt (1 + ((p3 `1) ^2))) ;
then A48: (f . p3) `2 < 0 by A44, A46, SQUARE_1:25, XREAL_1:141;
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:35;
W-min P = |[(- 1),0]| by A8, JGRAPH_5:29;
then f . p3 <> W-min P by A48, EUCLID:52;
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 Th1;
A52: - 1 <= p2 `2 by A50, Th1;
A53: p2 `2 <= 1 by A50, Th1;
(p2 `2) ^2 >= 0 by XREAL_1:63;
then A54: sqrt (1 + ((p2 `2) ^2)) > 0 by SQUARE_1:25;
p2 <> 0. (TOP-REAL 2) by A51, EUCLID:52, EUCLID:54;
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:52;
A57: (f . p2) `2 = (p2 `2) / (sqrt (1 + ((p2 `2) ^2))) by A51, A55, EUCLID:52;
now :: thesis: ( ( p3 in LSeg (|[1,1]|,|[1,(- 1)]|) & p2 `2 >= p3 `2 & LE f . p2,f . p3,P ) or ( p3 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p3 <> W-min (rectangle ((- 1),1,(- 1),1)) & LE f . p2,f . p3,P ) )
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, Th61;
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 Th1;
A60: - 1 <= p3 `2 by A58, Th1;
A61: p3 `2 <= 1 by A58, Th1;
(p3 `2) ^2 >= 0 by XREAL_1:63;
then A62: sqrt (1 + ((p3 `2) ^2)) > 0 by SQUARE_1:25;
p3 <> 0. (TOP-REAL 2) by A59, EUCLID:52, EUCLID:54;
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:52;
A65: (f . p3) `1 >= 0 by A59, A62, A63, EUCLID:52;
(p2 `2) * (sqrt (1 + ((p3 `2) ^2))) >= (p3 `2) * (sqrt (1 + ((p2 `2) ^2))) by A58, SQUARE_1:57;
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:72;
then p2 `2 >= ((p3 `2) * (sqrt (1 + ((p2 `2) ^2)))) / (sqrt (1 + ((p3 `2) ^2))) by A62, XCMPLX_1:89;
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:72;
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:89;
hence LE f . p2,f . p3,P by A8, A13, A14, A51, A54, A56, A57, A64, A65, JGRAPH_5:55; :: 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 Th3;
A68: - 1 <= p3 `1 by A66, Th3;
A69: p3 `1 <= 1 by A66, Th3;
A70: (p3 `1) ^2 >= 0 by XREAL_1:63;
then A71: sqrt (1 + ((p3 `1) ^2)) > 0 by SQUARE_1:25;
A72: - (p3 `2) >= p3 `1 by A66, A67, Th3;
p3 <> 0. (TOP-REAL 2) by A67, EUCLID:52, EUCLID:54;
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:4;
then A74: (f . p3) `1 = (p3 `1) / (sqrt (1 + (((p3 `1) / (- 1)) ^2))) by A67, EUCLID:52
.= (p3 `1) / (sqrt (1 + ((p3 `1) ^2))) ;
A75: (f . p3) `2 = (p3 `2) / (sqrt (1 + (((p3 `1) / (- 1)) ^2))) by A67, A73, EUCLID:52
.= (p3 `2) / (sqrt (1 + ((p3 `1) ^2))) ;
then A76: (f . p3) `2 < 0 by A67, A70, SQUARE_1:25, XREAL_1:141;
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:35;
W-min P = |[(- 1),0]| by A8, JGRAPH_5:29;
then A78: f . p3 <> W-min P by A76, EUCLID:52;
now :: thesis: ( ( (f . p2) `2 >= 0 & LE f . p2,f . p3,P ) or ( (f . p2) `2 < 0 & LE f . p2,f . p3,P ) )
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:34;
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:56, XREAL_1:72;
then p2 `1 >= ((p3 `1) * (sqrt (1 + ((p2 `2) ^2)))) / (sqrt (1 + ((p3 `1) ^2))) by A71, XCMPLX_1:89;
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:72;
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:89;
hence LE f . p2,f . p3,P by A8, A13, A14, A56, A67, A71, A74, A75, A78, A79, JGRAPH_5:56; :: 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 Th3;
A82: - 1 <= p2 `1 by A80, Th3;
(p2 `1) ^2 >= 0 by XREAL_1:63;
then A83: sqrt (1 + ((p2 `1) ^2)) > 0 by SQUARE_1:25;
A84: - (p2 `2) >= p2 `1 by A80, A81, Th3;
p2 <> 0. (TOP-REAL 2) by A81, EUCLID:52, EUCLID:54;
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:4;
then A86: (f . p2) `1 = (p2 `1) / (sqrt (1 + (((p2 `1) / (- 1)) ^2))) by A81, EUCLID:52
.= (p2 `1) / (sqrt (1 + ((p2 `1) ^2))) ;
A87: (f . p2) `2 = (p2 `2) / (sqrt (1 + (((p2 `1) / (- 1)) ^2))) by A81, A85, EUCLID:52
.= (p2 `2) / (sqrt (1 + ((p2 `1) ^2))) ;
A88: W-min (rectangle ((- 1),1,(- 1),1)) = |[(- 1),(- 1)]| by Th46;
then A89: p3 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) by A6, A80, Th62;
A90: p2 `1 >= p3 `1 by A6, A80, A88, Th62;
A91: p3 `2 = - 1 by A89, Th3;
A92: - 1 <= p3 `1 by A89, Th3;
A93: (p3 `1) ^2 >= 0 by XREAL_1:63;
then A94: sqrt (1 + ((p3 `1) ^2)) > 0 by SQUARE_1:25;
A95: - (p3 `2) >= p3 `1 by A89, A91, Th3;
p3 <> 0. (TOP-REAL 2) by A91, EUCLID:52, EUCLID:54;
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:4;
then A97: (f . p3) `1 = (p3 `1) / (sqrt (1 + (((p3 `1) / (- 1)) ^2))) by A91, EUCLID:52
.= (p3 `1) / (sqrt (1 + ((p3 `1) ^2))) ;
(f . p3) `2 = (p3 `2) / (sqrt (1 + (((p3 `1) / (- 1)) ^2))) by A91, A96, EUCLID:52
.= (p3 `2) / (sqrt (1 + ((p3 `1) ^2))) ;
then A98: (f . p3) `2 < 0 by A91, A93, SQUARE_1:25, XREAL_1:141;
W-min P = |[(- 1),0]| by A8, JGRAPH_5:29;
then A99: f . p3 <> W-min P by A98, EUCLID:52;
(p2 `1) * (sqrt (1 + ((p3 `1) ^2))) >= (p3 `1) * (sqrt (1 + ((p2 `1) ^2))) by A90, SQUARE_1:57;
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:72;
then p2 `1 >= ((p3 `1) * (sqrt (1 + ((p2 `1) ^2)))) / (sqrt (1 + ((p3 `1) ^2))) by A94, XCMPLX_1:89;
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:72;
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:89;
hence LE f . p2,f . p3,P by A8, A13, A14, A81, A83, A86, A87, A97, A98, A99, JGRAPH_5:56; :: thesis: verum
end;
end;
end;
hence LE f . p2,f . p3,P ; :: thesis: verum