let p1, p2 be Point of (TOP-REAL 2); 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) holds
LE f . p1,f . p2,P
let P be 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) holds
LE f . p1,f . p2,P
let f be Function of (TOP-REAL 2),(TOP-REAL 2); ( 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) implies LE f . p1,f . p2,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)
; LE f . p1,f . p2,P
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 ( ( p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & p2 `2 >= p1 `2 & LE f . p1,f . p2,P ) or ( p2 in LSeg (|[(- 1),1]|,|[1,1]|) & LE f . p1,f . p2,P ) or ( p2 in LSeg (|[1,1]|,|[1,(- 1)]|) & LE f . p1,f . p2,P ) or ( p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p2 <> |[(- 1),(- 1)]| & LE f . p1,f . p2,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 A26:
(
p2 in LSeg (
|[(- 1),(- 1)]|,
|[(- 1),1]|) &
p2 `2 >= p1 `2 )
;
LE f . p1,f . p2,PA27:
(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;
verum end; case A36:
p2 in LSeg (
|[(- 1),1]|,
|[1,1]|)
;
LE f . p1,f . p2,Pthen 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;
verum end; case A44:
p2 in LSeg (
|[1,1]|,
|[1,(- 1)]|)
;
LE f . p1,f . p2,Pthen 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;
hence
LE f . p1,
f . p2,
P
;
verum end; case A53:
(
p2 in LSeg (
|[1,(- 1)]|,
|[(- 1),(- 1)]|) &
p2 <> |[(- 1),(- 1)]| )
;
LE f . p1,f . p2,Pthen 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;
verum end; end; end;
hence
LE f . p1,f . p2,P
; verum