let p1, p2 be Point of (TOP-REAL 2); :: thesis:
let P be non empty compact Subset of (TOP-REAL 2); :: thesis:
assume A1: ( 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 ) ) ; :: thesis:
then consider p3 being Point of (TOP-REAL 2) such that
A2: ( p3 = p1 & |.p3.| = 1 ) ;
consider p3 being Point of (TOP-REAL 2) such that
A3: ( p3 = p2 & |.p3.| = 1 ) by A1;
A4: - (p2 `2 ) > 0 by A1, XREAL_1:60;

A5: now

assume p1 `2 <= p2 `2 ; :: thesis:
then - (p1 `2 ) >= - (p2 `2 ) by XREAL_1:26;
then (- (p1 `2 )) ^2 >= (- (p2 `2 )) ^2 by A4, SQUARE_1:77;
then A6: (1 ^2 ) - ((- (p1 `2 )) ^2 ) <= (1 ^2 ) - ((- (p2 `2 )) ^2 ) by XREAL_1:15;
A7: 1 ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) by A2, JGRAPH_3:10;
then A8: (1 ^2 ) - ((- (p1 `2 )) ^2 ) = (- (p1 `1 )) ^2 ;
- (p1 `1 ) >= 0 by A1;
then A9: - (p1 `1 ) = sqrt ((1 ^2 ) - ((- (p1 `2 )) ^2 )) by A8, SQUARE_1:89;
1 ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) by A3, JGRAPH_3:10;
then A10: (1 ^2 ) - ((- (p2 `2 )) ^2 ) = (- (p2 `1 )) ^2 ;
- (p2 `1 ) >= 0 by A1;
then A11: - (p2 `1 ) = sqrt ((1 ^2 ) - ((- (p2 `2 )) ^2 )) by A10, SQUARE_1:89;
(1 ^2 ) - ((- (p1 `2 )) ^2 ) >= 0 by A7, XREAL_1:65;
then sqrt ((1 ^2 ) - ((- (p1 `2 )) ^2 )) <= sqrt ((1 ^2 ) - ((- (p2 `2 )) ^2 )) by A6, SQUARE_1:94;
hence p1 `1 >= p2 `1 by A9, A11, XREAL_1:26; :: thesis:

end;

A12: P is being_simple_closed_curve by A1, JGRAPH_3:36;
then A13: Lower_Arc P is_an_arc_of E-max P, W-min P by JORDAN6:def 9;
set P4 = Lower_Arc P;
A14: ( Lower_Arc P is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point (Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) by A12, JORDAN6:def 9;
A15: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A1, Th37;

A16: now

assume not p1 in Lower_Arc P ; :: thesis:
then p1 in Upper_Arc P by A1, A14, XBOOLE_0:def 3;
then consider p being Point of (TOP-REAL 2) such that
A17: ( p1 = p & p in P & p `2 >= 0 ) by A15;
thus contradiction by A1, A17; :: thesis:

end;

A18: now

assume not p2 in Lower_Arc P ; :: thesis:
then p2 in Upper_Arc P by A1, A14, XBOOLE_0:def 3;
then consider p being Point of (TOP-REAL 2) such that
A19: ( p2 = p & p in P & p `2 >= 0 ) by A15;
thus contradiction by A1, A19; :: thesis:

end;

A20: W-min P = |[(- 1),0 ]| by A1, Th32;
A21: E-max P = |[1,0 ]| by A1, Th33;

A22: now

assume A23: p2 = W-min P ; :: thesis:
W-min P = |[(- 1),0 ]| by A1, Th32;
hence contradiction by A1, A23, EUCLID:56; :: thesis:

end;

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

let g be Function of I[01] ,((TOP-REAL 2) | (Lower_Arc P)); :: thesis:
let s1, s2 be Real; :: thesis:
assume A24: ( 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 ) ; :: thesis:
then A25: dom g = [#] I[01] by TOPS_2:def 5
.= [.0 ,1.] by BORSUK_1:83 ;
reconsider g0 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
set K0 = Lower_Arc P;
reconsider g2 = g0 | (Lower_Arc P) as Function of ((TOP-REAL 2) | (Lower_Arc P)),R^1 by PRE_TOPC:30;
reconsider g3 = g2 as continuous Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace (- 1),1) by A1, Lm4;
E-max P in {(W-min P),(E-max P)} by TARSKI:def 2;
then A26: E-max P in Lower_Arc P by A14, XBOOLE_0:def 4;
W-min P in {(W-min P),(E-max P)} by TARSKI:def 2;
then A27: W-min P in Lower_Arc P by A14, XBOOLE_0:def 4;
A28: dom g3 = [#] ((TOP-REAL 2) | (Lower_Arc P)) by FUNCT_2:def 1;
A29: rng g3 = [#] (Closed-Interval-TSpace (- 1),1) by A1, Lm4;
A30: g3 is one-to-one by A1, Lm4;
( not Lower_Arc P is empty & Lower_Arc P is compact ) by A13, JORDAN5A:1;
then A31: (TOP-REAL 2) | (Lower_Arc P) is compact ;
Closed-Interval-TSpace (- 1),1 = TopSpaceMetr (Closed-Interval-MSpace (- 1),1) by TOPMETR:def 8;
then Closed-Interval-TSpace (- 1),1 is T_2 by PCOMPS_1:38;
then A32: g3 is being_homeomorphism by A28, A29, A30, A31, COMPTS_1:26;
reconsider h = g3 * g as Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace (- 1),1) by TOPMETR:27;
A33: h is being_homeomorphism by A24, A32, TOPMETR:27, TOPS_2:71;
A34: 0 in dom g by A25, XXREAL_1:1;
A35: 1 in dom g by A25, XXREAL_1:1;
A36: s1 in [.0 ,1.] by A24, XXREAL_1:1;
A37: s2 in [.0 ,1.] by A24, XXREAL_1:1;
A38: - 1 = |[(- 1),0 ]| `1 by EUCLID:56
.= proj1 . |[(- 1),0 ]| by PSCOMP_1:def 28
.= g3 . (g . 1) by A20, A24, A27, FUNCT_1:72
.= h . 1 by A35, FUNCT_1:23 ;
A39: 1 = |[1,0 ]| `1 by EUCLID:56
.= g0 . |[1,0 ]| by PSCOMP_1:def 28
.= g3 . |[1,0 ]| by A21, A26, FUNCT_1:72
.= h . 0 by A21, A24, A34, FUNCT_1:23 ;
A40: p1 `1 = g0 . p1 by PSCOMP_1:def 28
.= g3 . (g . s1) by A16, A24, FUNCT_1:72
.= h . s1 by A25, A36, FUNCT_1:23 ;
p2 `1 = proj1 . p2 by PSCOMP_1:def 28
.= g3 . (g . s2) by A18, A24, FUNCT_1:72
.= h . s2 by A25, A37, FUNCT_1:23 ;
hence s1 <= s2 by A1, A5, A33, A36, A37, A38, A39, A40, Th12; :: thesis:

end;

then ( 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 A16, A18, A22, JORDAN5C:def 3;
hence LE p1,p2,P by JORDAN6:def 10; :: thesis: