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