let p1, p2, p3 be Point of (); :: thesis: for P being non empty compact Subset of ()
for f being Function of (),() 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 (); :: thesis: for f being Function of (),() 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 (),(); :: 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 () : |.p.| = 1 } by ;
A9: p3 in rectangle ((- 1),1,(- 1),1) by ;
A10: p2 in rectangle ((- 1),1,(- 1),1) by ;
A11: f .: (rectangle ((- 1),1,(- 1),1)) = P by ;
A12: dom f = the carrier of () by FUNCT_2:def 1;
then A13: f . p2 in P by ;
A14: f . p3 in P by ;
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 ;
A18: p2 `1 <= 1 by ;
(p2 `1) ^2 >= 0 by XREAL_1:63;
then A19: sqrt (1 + ((p2 `1) ^2)) > 0 by SQUARE_1:25;
p2 <> 0. () by ;
then A20: f . p2 = |[((p2 `1) / (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) / (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| by ;
then A21: (f . p2) `1 = (p2 `1) / (sqrt (1 + ((p2 `1) ^2))) by ;
A22: (f . p2) `2 >= 0 by ;
then f . p2 in { p9 where p9 is Point of () : ( p9 in P & p9 `2 >= 0 ) } by A13;
then A23: f . p2 in Upper_Arc P by ;
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 ;
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 ;
A27: p3 `1 <= 1 by ;
(p3 `1) ^2 >= 0 by XREAL_1:63;
then A28: sqrt (1 + ((p3 `1) ^2)) > 0 by SQUARE_1:25;
p3 <> 0. () by ;
then A29: f . p3 = |[((p3 `1) / (sqrt (1 + (((p3 `1) / (p3 `2)) ^2)))),((p3 `2) / (sqrt (1 + (((p3 `1) / (p3 `2)) ^2))))]| by ;
then A30: (f . p3) `1 = (p3 `1) / (sqrt (1 + ((p3 `1) ^2))) by ;
A31: (f . p3) `2 >= 0 by ;
(p2 `1) * (sqrt (1 + ((p3 `1) ^2))) <= (p3 `1) * (sqrt (1 + ((p2 `1) ^2))) by ;
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 ;
then p2 `1 <= ((p3 `1) * (sqrt (1 + ((p2 `1) ^2)))) / (sqrt (1 + ((p3 `1) ^2))) by ;
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 ;
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 ;
hence LE f . p2,f . p3,P by ; :: 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 ;
A35: p3 `2 <= 1 by ;
(p3 `2) ^2 >= 0 by XREAL_1:63;
then A36: sqrt (1 + ((p3 `2) ^2)) > 0 by SQUARE_1:25;
p3 <> 0. () by ;
then f . p3 = |[((p3 `1) / (sqrt (1 + (((p3 `2) / (p3 `1)) ^2)))),((p3 `2) / (sqrt (1 + (((p3 `2) / (p3 `1)) ^2))))]| by ;
then A37: (f . p3) `1 = (p3 `1) / (sqrt (1 + ((p3 `2) ^2))) by ;
A38: - 1 <= - (p2 `1) by ;
A39: - (- 1) >= - (p2 `1) by ;
(p2 `1) ^2 = (- (p2 `1)) ^2 ;
then (- (- (p2 `1))) * (sqrt (1 + ((p3 `2) ^2))) <= sqrt (1 + ((p2 `1) ^2)) by ;
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 ;
then p2 `1 <= ((p3 `1) * (sqrt (1 + ((p2 `1) ^2)))) / (sqrt (1 + ((p3 `2) ^2))) by ;
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 ;
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 ;
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 ; :: 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 () : ( p9 in P & p9 `2 <= 0 ) } by A14;
then A42: f . p3 in Lower_Arc P by ;
W-min P = |[(- 1),0]| by ;
then f . p3 <> W-min P by ;
hence LE f . p2,f . p3,P by ; :: 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 ;
A46: (p3 `1) ^2 >= 0 by XREAL_1:63;
A47: - (p3 `2) >= p3 `1 by ;
p3 <> 0. () by ;
then f . p3 = |[((p3 `1) / (sqrt (1 + (((p3 `1) / (p3 `2)) ^2)))),((p3 `2) / (sqrt (1 + (((p3 `1) / (p3 `2)) ^2))))]| by ;
then (f . p3) `2 = (p3 `2) / (sqrt (1 + (((p3 `1) / (- 1)) ^2))) by
.= (p3 `2) / (sqrt (1 + ((p3 `1) ^2))) ;
then A48: (f . p3) `2 < 0 by ;
then f . p3 in { p9 where p9 is Point of () : ( p9 in P & p9 `2 <= 0 ) } by A14;
then A49: f . p3 in Lower_Arc P by ;
W-min P = |[(- 1),0]| by ;
then f . p3 <> W-min P by ;
hence LE f . p2,f . p3,P by ; :: 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 ;
A53: p2 `2 <= 1 by ;
(p2 `2) ^2 >= 0 by XREAL_1:63;
then A54: sqrt (1 + ((p2 `2) ^2)) > 0 by SQUARE_1:25;
p2 <> 0. () by ;
then A55: f . p2 = |[((p2 `1) / (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) / (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]| by ;
then A56: (f . p2) `1 = (p2 `1) / (sqrt (1 + ((p2 `2) ^2))) by ;
A57: (f . p2) `2 = (p2 `2) / (sqrt (1 + ((p2 `2) ^2))) by ;
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 ;
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 ;
A61: p3 `2 <= 1 by ;
(p3 `2) ^2 >= 0 by XREAL_1:63;
then A62: sqrt (1 + ((p3 `2) ^2)) > 0 by SQUARE_1:25;
p3 <> 0. () by ;
then A63: f . p3 = |[((p3 `1) / (sqrt (1 + (((p3 `2) / (p3 `1)) ^2)))),((p3 `2) / (sqrt (1 + (((p3 `2) / (p3 `1)) ^2))))]| by ;
then A64: (f . p3) `2 = (p3 `2) / (sqrt (1 + ((p3 `2) ^2))) by ;
A65: (f . p3) `1 >= 0 by ;
(p2 `2) * (sqrt (1 + ((p3 `2) ^2))) >= (p3 `2) * (sqrt (1 + ((p2 `2) ^2))) by ;
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 ;
then p2 `2 >= ((p3 `2) * (sqrt (1 + ((p2 `2) ^2)))) / (sqrt (1 + ((p3 `2) ^2))) by ;
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 ;
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 ;
hence LE f . p2,f . p3,P by ; :: 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 ;
A69: p3 `1 <= 1 by ;
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 ;
p3 <> 0. () by ;
then A73: f . p3 = |[((p3 `1) / (sqrt (1 + (((p3 `1) / (p3 `2)) ^2)))),((p3 `2) / (sqrt (1 + (((p3 `1) / (p3 `2)) ^2))))]| by ;
then A74: (f . p3) `1 = (p3 `1) / (sqrt (1 + (((p3 `1) / (- 1)) ^2))) by
.= (p3 `1) / (sqrt (1 + ((p3 `1) ^2))) ;
A75: (f . p3) `2 = (p3 `2) / (sqrt (1 + (((p3 `1) / (- 1)) ^2))) by
.= (p3 `2) / (sqrt (1 + ((p3 `1) ^2))) ;
then A76: (f . p3) `2 < 0 by ;
f . p3 in { p9 where p9 is Point of () : ( p9 in P & p9 `2 <= 0 ) } by A14, A67, A71, A75;
then A77: f . p3 in Lower_Arc P by ;
W-min P = |[(- 1),0]| by ;
then A78: f . p3 <> W-min P by ;
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 () : ( p9 in P & p9 `2 >= 0 ) } by A13;
then f . p2 in Upper_Arc P by ;
hence LE f . p2,f . p3,P by ; :: 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 ;
then p2 `1 >= ((p3 `1) * (sqrt (1 + ((p2 `2) ^2)))) / (sqrt (1 + ((p3 `1) ^2))) by ;
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 ;
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 ;
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 ;
(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 ;
p2 <> 0. () by ;
then A85: f . p2 = |[((p2 `1) / (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) / (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]| by ;
then A86: (f . p2) `1 = (p2 `1) / (sqrt (1 + (((p2 `1) / (- 1)) ^2))) by
.= (p2 `1) / (sqrt (1 + ((p2 `1) ^2))) ;
A87: (f . p2) `2 = (p2 `2) / (sqrt (1 + (((p2 `1) / (- 1)) ^2))) by
.= (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 ;
A90: p2 `1 >= p3 `1 by A6, A80, A88, Th62;
A91: p3 `2 = - 1 by ;
A92: - 1 <= p3 `1 by ;
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 ;
p3 <> 0. () by ;
then A96: f . p3 = |[((p3 `1) / (sqrt (1 + (((p3 `1) / (p3 `2)) ^2)))),((p3 `2) / (sqrt (1 + (((p3 `1) / (p3 `2)) ^2))))]| by ;
then A97: (f . p3) `1 = (p3 `1) / (sqrt (1 + (((p3 `1) / (- 1)) ^2))) by
.= (p3 `1) / (sqrt (1 + ((p3 `1) ^2))) ;
(f . p3) `2 = (p3 `2) / (sqrt (1 + (((p3 `1) / (- 1)) ^2))) by
.= (p3 `2) / (sqrt (1 + ((p3 `1) ^2))) ;
then A98: (f . p3) `2 < 0 by ;
W-min P = |[(- 1),0]| by ;
then A99: f . p3 <> W-min P by ;
(p2 `1) * (sqrt (1 + ((p3 `1) ^2))) >= (p3 `1) * (sqrt (1 + ((p2 `1) ^2))) by ;
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 ;
then p2 `1 >= ((p3 `1) * (sqrt (1 + ((p2 `1) ^2)))) / (sqrt (1 + ((p3 `1) ^2))) by ;
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 ;
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 ;
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