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 & p2 `1 < 0 & p1 `2 >= 0 & p2 `2 >= 0 holds
( p1 `1 < p2 `1 & 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 & p2 `1 < 0 & p1 `2 >= 0 & p2 `2 >= 0 implies ( p1 `1 < p2 `1 & 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:
p2 `1 < 0
and
A5:
p1 `2 >= 0
and
A6:
p2 `2 >= 0
; ( p1 `1 < p2 `1 & p1 `2 < p2 `2 )
set P4 = Lower_Arc P;
A7:
P is being_simple_closed_curve
by A1, JGRAPH_3:26;
then A8:
(Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)}
by JORDAN6:def 9;
A9:
p1 in P
by A2, A7, JORDAN7:5;
A11:
p2 in P
by A2, A7, JORDAN7:5;
then
ex p4 being Point of (TOP-REAL 2) st
( p4 = p2 & |.p4.| = 1 )
by A1;
then
1 ^2 = ((p2 `1) ^2) + ((p2 `2) ^2)
by JGRAPH_3:1;
then A12:
p2 `2 = sqrt ((1 ^2) - ((- (p2 `1)) ^2))
by A6, SQUARE_1:22;
A13:
Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
by A1, Th34;
A14:
now not p2 in Lower_Arc Passume A15:
p2 in Lower_Arc P
;
contradiction
p2 in Upper_Arc P
by A6, A11, A13;
then
p2 in {(W-min P),(E-max P)}
by A8, A15, XBOOLE_0:def 4;
then A16:
(
p2 = W-min P or
p2 = E-max P )
by TARSKI:def 2;
E-max P = |[1,0]|
by A1, Th30;
hence
contradiction
by A4, A10, A16, EUCLID:52;
verum end;
then A17:
LE p1,p2, Upper_Arc P, W-min P, E-max P
by A2;
A18:
ex p3 being Point of (TOP-REAL 2) st
( p3 = p1 & |.p3.| = 1 )
by A1, A9;
then
1 ^2 = ((p1 `1) ^2) + ((p1 `2) ^2)
by JGRAPH_3:1;
then A19:
p1 `2 = sqrt ((1 ^2) - ((- (p1 `1)) ^2))
by A5, SQUARE_1:22;
1 ^2 = ((p1 `1) ^2) + ((p1 `2) ^2)
by A18, JGRAPH_3:1;
then A20:
(1 ^2) - ((- (p1 `1)) ^2) >= 0
by XREAL_1:63;
consider f being Function of I[01],((TOP-REAL 2) | (Upper_Arc P)) such that
A21:
f is being_homeomorphism
and
A22:
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
A23:
( f . 0 = W-min P & f . 1 = E-max P )
by A1, Th43;
A24: rng f =
[#] ((TOP-REAL 2) | (Upper_Arc P))
by A21, TOPS_2:def 5
.=
Upper_Arc P
by PRE_TOPC:def 5
;
p2 in Upper_Arc P
by A2, A14;
then consider x2 being object such that
A25:
x2 in dom f
and
A26:
p2 = f . x2
by A24, FUNCT_1:def 3;
A27: dom f =
[#] I[01]
by A21, TOPS_2:def 5
.=
[.0,1.]
by BORSUK_1:40
;
reconsider r22 = x2 as Real by A25;
A28:
( 0 <= r22 & r22 <= 1 )
by A25, A27, XXREAL_1:1;
p1 in Upper_Arc P
by A2, A14;
then consider x1 being object such that
A29:
x1 in dom f
and
A30:
p1 = f . x1
by A24, FUNCT_1:def 3;
reconsider r11 = x1 as Real by A29;
r11 <= 1
by A29, A27, XXREAL_1:1;
then A31:
r11 <= r22
by A17, A21, A23, A30, A26, A28, JORDAN5C:def 3;
A32:
( r11 < r22 iff p1 `1 < p2 `1 )
by A22, A29, A30, A25, A26, A27;
then
- (p1 `1) > - (p2 `1)
by A3, A30, A26, A31, XREAL_1:24, XXREAL_0:1;
then
(- (p1 `1)) ^2 > (- (p2 `1)) ^2
by A4, SQUARE_1:16;
then
(1 ^2) - ((- (p1 `1)) ^2) < (1 ^2) - ((- (p2 `1)) ^2)
by XREAL_1:15;
hence
( p1 `1 < p2 `1 & p1 `2 < p2 `2 )
by A30, A26, A32, A31, A19, A12, A20, SQUARE_1:27, XXREAL_0:1; verum