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 `2 >= 0 holds
p1 `1 < p2 `1
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 `2 >= 0 implies p1 `1 < p2 `1 )
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 `2 >= 0
; p1 `1 < p2 `1
A5:
P is being_simple_closed_curve
by A1, JGRAPH_3:36;
then A6:
p1 in P
by A2, JORDAN7:5;
set P4 = Lower_Arc P;
A7:
Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
by A1, Th37;
A8:
(Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)}
by A5, JORDAN6:def 9;
A9:
p2 in P
by A2, A5, JORDAN7:5;
A10:
now assume A12:
p2 in Lower_Arc P
;
p1 `1 < p2 `1
p2 in Upper_Arc P
by A4, A9, A7;
then
p2 in {(W-min P),(E-max P)}
by A8, A12, XBOOLE_0:def 4;
then
(
p2 = W-min P or
p2 = E-max P )
by TARSKI:def 2;
then A13:
p2 = |[1,0]|
by A1, A11, Th33;
then A14:
p2 `1 = 1
by EUCLID:56;
A15:
ex
p8 being
Point of
(TOP-REAL 2) st
(
p8 = p1 &
|.p8.| = 1 )
by A1, A6;
p1 `1 <= 1
by A15, Th3;
hence
p1 `1 < p2 `1
by A14, A16, XXREAL_0:1;
verum end;
then A18:
( ( p1 in Upper_Arc P & p2 in Upper_Arc P & not p2 = W-min P & LE p1,p2, Upper_Arc P, W-min P, E-max P ) or p1 `1 < p2 `1 )
by A2, A10, JORDAN6:def 10;
consider f being Function of I[01],((TOP-REAL 2) | (Upper_Arc P)) such that
A19:
f is being_homeomorphism
and
A20:
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
A21:
( f . 0 = W-min P & f . 1 = E-max P )
by A1, Th46;
A22: rng f =
[#] ((TOP-REAL 2) | (Upper_Arc P))
by A19, TOPS_2:def 5
.=
Upper_Arc P
by PRE_TOPC:def 10
;
now per cases
( not p1 `1 < p2 `1 or p1 `1 < p2 `1 )
;
case A23:
not
p1 `1 < p2 `1
;
p1 `1 < p2 `1 then consider x1 being
set such that A24:
x1 in dom f
and A25:
p1 = f . x1
by A18, A22, FUNCT_1:def 5;
consider x2 being
set such that A26:
x2 in dom f
and A27:
p2 = f . x2
by A18, A22, A23, FUNCT_1:def 5;
A28:
dom f =
[#] I[01]
by A19, TOPS_2:def 5
.=
[.0,1.]
by BORSUK_1:83
;
then reconsider r22 =
x2 as
Real by A26;
A29:
(
0 <= r22 &
r22 <= 1 )
by A26, A28, XXREAL_1:1;
reconsider r11 =
x1 as
Real by A24, A28;
A30:
(
r11 < r22 iff
p1 `1 < p2 `1 )
by A20, A24, A25, A26, A27, A28;
r11 <= 1
by A24, A28, XXREAL_1:1;
then
(
r11 <= r22 or
p1 `1 < p2 `1 )
by A18, A19, A21, A25, A27, A29, JORDAN5C:def 3;
hence
p1 `1 < p2 `1
by A3, A25, A27, A30, XXREAL_0:1;
verum end;
hence
p1 `1 < p2 `1
; verum