let p1, p2, p3 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) & 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); 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); ( 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)
; 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 ( ( 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 A15:
p2 in LSeg (
|[(- 1),1]|,
|[1,1]|)
;
LE f . p2,f . p3,Pthen 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 ( ( 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 )
;
LE f . p2,f . p3,Pthen 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;
verum end; case A32:
p3 in LSeg (
|[1,1]|,
|[1,(- 1)]|)
;
LE f . p2,f . p3,Pthen 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;
hence
LE f . p2,
f . p3,
P
;
verum end; case A43:
(
p3 in LSeg (
|[1,(- 1)]|,
|[(- 1),(- 1)]|) &
p3 <> W-min (rectangle ((- 1),1,(- 1),1)) )
;
LE f . p2,f . p3,Pthen 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;
verum end; end; end; hence
LE f . p2,
f . p3,
P
;
verum end; case A50:
p2 in LSeg (
|[1,1]|,
|[1,(- 1)]|)
;
LE f . p2,f . p3,Pthen 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 ( ( 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 )
;
LE f . p2,f . p3,Pthen 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;
verum end; case A66:
(
p3 in LSeg (
|[1,(- 1)]|,
|[(- 1),(- 1)]|) &
p3 <> W-min (rectangle ((- 1),1,(- 1),1)) )
;
LE f . p2,f . p3,Pthen 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 ( ( (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 A79:
(f . p2) `2 < 0
;
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;
verum end; end; end; hence
LE f . p2,
f . p3,
P
;
verum end; end; end; hence
LE f . p2,
f . p3,
P
;
verum end; case A80:
(
p2 in LSeg (
|[1,(- 1)]|,
|[(- 1),(- 1)]|) &
p2 <> |[(- 1),(- 1)]| )
;
LE f . p2,f . p3,Pthen 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;
verum end; end; end;
hence
LE f . p2,f . p3,P
; verum