let p1, p2 be Point of (TOP-REAL 2); for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & p1 <> p2 & p1 `1 >= 0 & p2 `1 >= 0 holds
p1 `2 > p2 `2
let P be non empty compact Subset of (TOP-REAL 2); ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & p1 <> p2 & p1 `1 >= 0 & p2 `1 >= 0 implies p1 `2 > p2 `2 )
assume that
A1:
P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 }
and
A2:
LE p1,p2,P
and
A3:
p1 <> p2
and
A4:
p1 `1 >= 0
and
A5:
p2 `1 >= 0
; p1 `2 > p2 `2
A6:
Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
by A1, Th37;
A7:
P is being_simple_closed_curve
by A1, JGRAPH_3:36;
then A8:
p2 in P
by A2, JORDAN7:5;
then A9:
ex p3 being Point of (TOP-REAL 2) st
( p3 = p2 & |.p3.| = 1 )
by A1;
W-min P = |[(- 1),0]|
by A1, Th32;
then A10:
(W-min P) `2 = 0
by EUCLID:56;
A11:
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) }
by A1, Th38;
A12:
p1 in P
by A2, A7, JORDAN7:5;
then A13:
ex p4 being Point of (TOP-REAL 2) st
( p4 = p1 & |.p4.| = 1 )
by A1;
now per cases
( ( p1 `2 >= 0 & p2 `2 >= 0 ) or ( p1 `2 >= 0 & p2 `2 < 0 ) or ( p1 `2 < 0 & p2 `2 >= 0 ) or ( p1 `2 < 0 & p2 `2 < 0 ) )
;
case A14:
(
p1 `2 >= 0 &
p2 `2 >= 0 )
;
p1 `2 > p2 `2 then
p1 `1 < p2 `1
by A1, A2, A3, Th50;
then
(p1 `1) ^2 < (p2 `1) ^2
by A4, SQUARE_1:78;
then A15:
(1 ^2) - ((p1 `1) ^2) > (1 ^2) - ((p2 `1) ^2)
by XREAL_1:17;
1
^2 = ((p1 `1) ^2) + ((p1 `2) ^2)
by A13, JGRAPH_3:10;
then A16:
p1 `2 = sqrt ((1 ^2) - ((p1 `1) ^2))
by A14, SQUARE_1:89;
A17:
1
^2 = ((p2 `1) ^2) + ((p2 `2) ^2)
by A9, JGRAPH_3:10;
then
p2 `2 = sqrt ((1 ^2) - ((p2 `1) ^2))
by A14, SQUARE_1:89;
hence
p1 `2 > p2 `2
by A15, A16, A17, SQUARE_1:95, XREAL_1:65;
verum end; case A18:
(
p1 `2 < 0 &
p2 `2 >= 0 )
;
contradictionthen
(
p1 in Lower_Arc P &
p2 in Upper_Arc P )
by A12, A8, A6, A11;
then
LE p2,
p1,
P
by A10, A18, JORDAN6:def 10;
hence
contradiction
by A1, A2, A3, JGRAPH_3:36, JORDAN6:72;
verum end; case A19:
(
p1 `2 < 0 &
p2 `2 < 0 )
;
p1 `2 > p2 `2
ex
p3 being
Point of
(TOP-REAL 2) st
(
p3 = p1 &
|.p3.| = 1 )
by A1, A12;
then A20:
1
^2 = ((p1 `1) ^2) + ((p1 `2) ^2)
by JGRAPH_3:10;
then
(1 ^2) - ((p1 `1) ^2) = (- (p1 `2)) ^2
;
then A21:
- (p1 `2) = sqrt ((1 ^2) - ((p1 `1) ^2))
by A19, SQUARE_1:89;
for
p being
Point of
(TOP-REAL 2) holds
( not
p = p1 or not
p in P or not
p `2 >= 0 )
by A19;
then A22:
not
p1 in Upper_Arc P
by A6;
then A23:
LE p1,
p2,
Lower_Arc P,
E-max P,
W-min P
by A2, JORDAN6:def 10;
ex
p4 being
Point of
(TOP-REAL 2) st
(
p4 = p2 &
|.p4.| = 1 )
by A1, A8;
then
1
^2 = ((p2 `1) ^2) + ((p2 `2) ^2)
by JGRAPH_3:10;
then
(1 ^2) - ((p2 `1) ^2) = (- (p2 `2)) ^2
;
then A24:
- (p2 `2) = sqrt ((1 ^2) - ((p2 `1) ^2))
by A19, SQUARE_1:89;
consider f being
Function of
I[01],
((TOP-REAL 2) | (Lower_Arc P)) such that A25:
f is
being_homeomorphism
and A26:
for
q1,
q2 being
Point of
(TOP-REAL 2) for
r1,
r2 being
Real st
f . r1 = q1 &
f . r2 = q2 &
r1 in [.0,1.] &
r2 in [.0,1.] holds
(
r1 < r2 iff
q1 `1 > q2 `1 )
and A27:
(
f . 0 = E-max P &
f . 1
= W-min P )
by A1, Th45;
A28:
rng f =
[#] ((TOP-REAL 2) | (Lower_Arc P))
by A25, TOPS_2:def 5
.=
Lower_Arc P
by PRE_TOPC:def 10
;
p2 in Lower_Arc P
by A2, A22, JORDAN6:def 10;
then consider x2 being
set such that A29:
x2 in dom f
and A30:
p2 = f . x2
by A28, FUNCT_1:def 5;
A31:
dom f =
[#] I[01]
by A25, TOPS_2:def 5
.=
[.0,1.]
by BORSUK_1:83
;
then reconsider r22 =
x2 as
Real by A29;
A32:
(
0 <= r22 &
r22 <= 1 )
by A29, A31, XXREAL_1:1;
p1 in Lower_Arc P
by A2, A22, JORDAN6:def 10;
then consider x1 being
set such that A33:
x1 in dom f
and A34:
p1 = f . x1
by A28, FUNCT_1:def 5;
reconsider r11 =
x1 as
Real by A33, A31;
A35:
(
r11 < r22 iff
p1 `1 > p2 `1 )
by A26, A33, A34, A29, A30, A31;
r11 <= 1
by A33, A31, XXREAL_1:1;
then
r11 <= r22
by A23, A25, A27, A34, A30, A32, JORDAN5C:def 3;
then
(p1 `1) ^2 > (p2 `1) ^2
by A3, A5, A34, A30, A35, SQUARE_1:78, XXREAL_0:1;
then
(1 ^2) - ((p1 `1) ^2) < (1 ^2) - ((p2 `1) ^2)
by XREAL_1:17;
then
sqrt ((1 ^2) - ((p1 `1) ^2)) < sqrt ((1 ^2) - ((p2 `1) ^2))
by A20, SQUARE_1:95, XREAL_1:65;
hence
p1 `2 > p2 `2
by A21, A24, XREAL_1:26;
verum
hence
p1 `2 > p2 `2
; verum