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 } & p1 in P & p2 in P & p1 `1 > 0 & p2 `1 > 0 & p1 `2 < 0 & p2 `2 < 0 & ( p1 `1 >= p2 `1 or p1 `2 >= p2 `2 ) holds
LE p1,p2,P
let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p1 `1 > 0 & p2 `1 > 0 & p1 `2 < 0 & p2 `2 < 0 & ( p1 `1 >= p2 `1 or p1 `2 >= p2 `2 ) implies LE p1,p2,P )
assume that
A1: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } and
A2: p1 in P and
A3: p2 in P and
A4: p1 `1 > 0 and
A5: p2 `1 > 0 and
A6: p1 `2 < 0 and
A7: p2 `2 < 0 and
A8: ( p1 `1 >= p2 `1 or p1 `2 >= p2 `2 ) ; :: thesis: LE p1,p2,P
A9: ex p3 being Point of (TOP-REAL 2) st
( p3 = p2 & |.p3.| = 1 ) by A1, A3;
set P4 = Lower_Arc P;
A10: P is being_simple_closed_curve by A1, JGRAPH_3:26;
then A11: (Upper_Arc P) \/ (Lower_Arc P) = P by JORDAN6:def 9;
A12: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A1, Th34;

A13: now :: thesis: p1 in Lower_Arc P

assume not p1 in Lower_Arc P ; :: thesis: contradiction
then p1 in Upper_Arc P by A2, A11, XBOOLE_0:def 3;
then ex p being Point of (TOP-REAL 2) st
( p1 = p & p in P & p `2 >= 0 ) by A12;
hence contradiction by A6; :: thesis: verum

end;

A14: now :: thesis: p2 in Lower_Arc P

assume not p2 in Lower_Arc P ; :: thesis: contradiction
then p2 in Upper_Arc P by A3, A11, XBOOLE_0:def 3;
then ex p being Point of (TOP-REAL 2) st
( p2 = p & p in P & p `2 >= 0 ) by A12;
hence contradiction by A7; :: thesis: verum

end;

A15: ex p3 being Point of (TOP-REAL 2) st
( p3 = p1 & |.p3.| = 1 ) by A1, A2;

A16: now :: thesis: ( p1 `2 >= p2 `2 implies p1 `1 >= p2 `1 )

assume p1 `2 >= p2 `2 ; :: thesis: p1 `1 >= p2 `1
then - (p1 `2) <= - (p2 `2) by XREAL_1:24;
then (- (p1 `2)) ^2 <= (- (p2 `2)) ^2 by A6, SQUARE_1:15;
then A17: (1 ^2) - ((- (p1 `2)) ^2) >= (1 ^2) - ((- (p2 `2)) ^2) by XREAL_1:13;
1 ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by A9, JGRAPH_3:1;
then A18: ( p2 `1 = sqrt ((1 ^2) - ((- (p2 `2)) ^2)) & (1 ^2) - ((- (p2 `2)) ^2) >= 0 ) by A5, SQUARE_1:22;
1 ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by A15, JGRAPH_3:1;
then p1 `1 = sqrt ((1 ^2) - ((- (p1 `2)) ^2)) by A4, SQUARE_1:22;
hence p1 `1 >= p2 `1 by A17, A18, SQUARE_1:26; :: thesis: verum

end;

A19: (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} by A10, JORDAN6:def 9;
A20: Lower_Arc P is_an_arc_of E-max P, W-min P by A10, JORDAN6:def 9;
A21: W-min P = |[(- 1),0]| by A1, Th29;
for g being Function of I[01],((TOP-REAL 2) | (Lower_Arc P))
for s1, s2 being Real st g is being_homeomorphism & g . 0 = E-max P & g . 1 = W-min P & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2

proof

W-min P in {(W-min P),(E-max P)} by TARSKI:def 2;
then A22: W-min P in Lower_Arc P by A19, XBOOLE_0:def 4;
set K0 = Lower_Arc P;
reconsider g0 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
reconsider g2 = g0 | (Lower_Arc P) as Function of ((TOP-REAL 2) | (Lower_Arc P)),R^1 by PRE_TOPC:9;
Closed-Interval-TSpace ((- 1),1) = TopSpaceMetr (Closed-Interval-MSpace ((- 1),1)) by TOPMETR:def 7;
then A23: Closed-Interval-TSpace ((- 1),1) is T_2 by PCOMPS_1:34;
reconsider g3 = g2 as continuous Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace ((- 1),1)) by A1, Lm5;
let g be Function of I[01],((TOP-REAL 2) | (Lower_Arc P)); :: thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = E-max P & g . 1 = W-min P & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2
let s1, s2 be Real; :: thesis: ( g is being_homeomorphism & g . 0 = E-max P & g . 1 = W-min P & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume that
A24: g is being_homeomorphism and
g . 0 = E-max P and
A25: g . 1 = W-min P and
A26: g . s1 = p1 and
A27: ( 0 <= s1 & s1 <= 1 ) and
A28: g . s2 = p2 and
A29: ( 0 <= s2 & s2 <= 1 ) ; :: thesis: s1 <= s2
A30: s2 in [.0,1.] by A29, XXREAL_1:1;
reconsider h = g3 * g as Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace ((- 1),1)) by TOPMETR:20;
A31: ( dom g3 = [#] ((TOP-REAL 2) | (Lower_Arc P)) & rng g3 = [#] (Closed-Interval-TSpace ((- 1),1)) ) by A1, Lm5, FUNCT_2:def 1;
( g3 is one-to-one & not Lower_Arc P is empty & Lower_Arc P is compact ) by A1, A20, Lm5, JORDAN5A:1;
then g3 is being_homeomorphism by A31, A23, COMPTS_1:17;
then A32: h is being_homeomorphism by A24, TOPMETR:20, TOPS_2:57;
A33: dom g = [#] I[01] by A24, TOPS_2:def 5
.= [.0,1.] by BORSUK_1:40 ;
then A34: 1 in dom g by XXREAL_1:1;
A35: - 1 = |[(- 1),0]| `1 by EUCLID:52
.= proj1 . |[(- 1),0]| by PSCOMP_1:def 5
.= g3 . (g . 1) by A21, A25, A22, FUNCT_1:49
.= h . 1 by A34, FUNCT_1:13 ;
A36: s1 in [.0,1.] by A27, XXREAL_1:1;
A37: p2 `1 = proj1 . p2 by PSCOMP_1:def 5
.= g3 . p2 by A14, FUNCT_1:49
.= h . s2 by A28, A33, A30, FUNCT_1:13 ;
p1 `1 = g0 . p1 by PSCOMP_1:def 5
.= g3 . (g . s1) by A13, A26, FUNCT_1:49
.= h . s1 by A33, A36, FUNCT_1:13 ;
hence s1 <= s2 by A8, A16, A32, A36, A30, A35, A37, Th9; :: thesis: verum

end;

then A38: LE p1,p2, Lower_Arc P, E-max P, W-min P by A13, A14, JORDAN5C:def 3;

now :: thesis: not p2 = W-min P

assume A39: p2 = W-min P ; :: thesis: contradiction
W-min P = |[(- 1),0]| by A1, Th29;
hence contradiction by A5, A39, EUCLID:52; :: thesis: verum

end;

hence LE p1,p2,P by A13, A14, A38; :: thesis: verum