let p1, p2 be Point of (TOP-REAL 2); :: thesis:
let P be non empty compact Subset of (TOP-REAL 2); :: thesis:
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 >= p2 `2 ; :: thesis:
A7: ex p3 being Point of (TOP-REAL 2) st
( p3 = p1 & |.p3.| = 1 ) by A1, A2;
A8: W-min P = |[(- 1),0]| by A1, Th29;
A9: ex p3 being Point of (TOP-REAL 2) st
( p3 = p2 & |.p3.| = 1 ) by A1, A3;
A10: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A1, Th34;
set P4b = Lower_Arc P;
A11: P is being_simple_closed_curve by A1, JGRAPH_3:26;
then A12: (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} by JORDAN6:def 9;
A13: (Upper_Arc P) \/ (Lower_Arc P) = P by A11, JORDAN6:def 9;
A14: Lower_Arc P is_an_arc_of E-max P, W-min P by A11, JORDAN6:def 9;

now :: thesis:

per cases ;

case A15: ( p1 in Upper_Arc P & p2 in Upper_Arc P ) ; :: thesis:

1 ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by A7, JGRAPH_3:1;
then A16: ( p1 `1 = sqrt ((1 ^2) - ((p1 `2) ^2)) & (1 ^2) - ((p1 `2) ^2) >= 0 ) by A4, SQUARE_1:22;
1 ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by A9, JGRAPH_3:1;
then A17: p2 `1 = sqrt ((1 ^2) - ((p2 `2) ^2)) by A5, SQUARE_1:22;
A18: ex p22 being Point of (TOP-REAL 2) st
( p2 = p22 & p22 in P & p22 `2 >= 0 ) by A10, A15;
then (p1 `2) ^2 >= (p2 `2) ^2 by A6, SQUARE_1:15;
then (1 ^2) - ((p1 `2) ^2) <= (1 ^2) - ((p2 `2) ^2) by XREAL_1:13;
hence LE p1,p2,P by A1, A2, A6, A18, A17, A16, Th54, SQUARE_1:26; :: thesis:

end;

case A19: ( p1 in Upper_Arc P & not p2 in Upper_Arc P ) ; :: thesis:

A20: now :: thesis:

assume A21: p2 = W-min P ; :: thesis:
W-min P = |[(- 1),0]| by A1, Th29;
then p2 `2 = 0 by A21, EUCLID:52;
hence contradiction by A3, A10, A19; :: thesis:

end;

p2 in Lower_Arc P by A3, A13, A19, XBOOLE_0:def 3;
hence LE p1,p2,P by A19, A20; :: thesis:

end;

case A22: ( not p1 in Upper_Arc P & p2 in Upper_Arc P ) ; :: thesis:

then ex p9 being Point of (TOP-REAL 2) st
( p2 = p9 & p9 in P & p9 `2 >= 0 ) by A10;
hence contradiction by A2, A6, A10, A22; :: thesis:

end;

case A23: ( not p1 in Upper_Arc P & not p2 in Upper_Arc P ) ; :: thesis:

A24: - (p1 `2) <= - (p2 `2) by A6, XREAL_1:24;
p1 `2 < 0 by A2, A10, A23;
then (- (p1 `2)) ^2 <= (- (p2 `2)) ^2 by A24, SQUARE_1:15;
then A25: (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 A26: ( p2 `1 = sqrt ((1 ^2) - ((- (p2 `2)) ^2)) & (1 ^2) - ((- (p2 `2)) ^2) >= 0 ) by A5, SQUARE_1:22;
A27: p2 in Lower_Arc P by A3, A13, A23, XBOOLE_0:def 3;

A28: now :: thesis:

assume A29: p2 = W-min P ; :: thesis:
W-min P = |[(- 1),0]| by A1, Th29;
then p2 `2 = 0 by A29, EUCLID:52;
hence contradiction by A3, A10, A23; :: thesis:

end;

A30: p1 in Lower_Arc P by A2, A13, A23, XBOOLE_0:def 3;
1 ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by A7, JGRAPH_3:1;
then p1 `1 = sqrt ((1 ^2) - ((- (p1 `2)) ^2)) by A4, SQUARE_1:22;
then A31: p1 `1 >= p2 `1 by A25, A26, SQUARE_1:26;
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 A32: W-min P in Lower_Arc P by A12, 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 A33: 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:
let s1, s2 be Real; :: thesis:
assume that
A34: g is being_homeomorphism and
g . 0 = E-max P and
A35: g . 1 = W-min P and
A36: g . s1 = p1 and
A37: ( 0 <= s1 & s1 <= 1 ) and
A38: g . s2 = p2 and
A39: ( 0 <= s2 & s2 <= 1 ) ; :: thesis:
A40: s2 in [.0,1.] by A39, XXREAL_1:1;
reconsider h = g3 * g as Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace ((- 1),1)) by TOPMETR:20;
A41: ( 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, A14, Lm5, JORDAN5A:1;
then g3 is being_homeomorphism by A41, A33, COMPTS_1:17;
then A42: h is being_homeomorphism by A34, TOPMETR:20, TOPS_2:57;
A43: dom g = [#] I[01] by A34, TOPS_2:def 5
.= [.0,1.] by BORSUK_1:40 ;
then A44: 1 in dom g by XXREAL_1:1;
A45: - 1 = |[(- 1),0]| `1 by EUCLID:52
.= proj1 . |[(- 1),0]| by PSCOMP_1:def 5
.= g3 . |[(- 1),0]| by A8, A32, FUNCT_1:49
.= h . 1 by A8, A35, A44, FUNCT_1:13 ;
A46: s1 in [.0,1.] by A37, XXREAL_1:1;
A47: p2 `1 = g0 . p2 by PSCOMP_1:def 5
.= g3 . p2 by A27, FUNCT_1:49
.= h . s2 by A38, A43, A40, FUNCT_1:13 ;
p1 `1 = g0 . p1 by PSCOMP_1:def 5
.= g3 . p1 by A30, FUNCT_1:49
.= h . s1 by A36, A43, A46, FUNCT_1:13 ;
hence s1 <= s2 by A31, A42, A46, A40, A45, A47, Th9; :: thesis:

end;

then A48: LE p1,p2, Lower_Arc P, E-max P, W-min P by A30, A27, JORDAN5C:def 3;
p1 in Lower_Arc P by A2, A13, A23, XBOOLE_0:def 3;
hence LE p1,p2,P by A27, A28, A48; :: thesis:

end;

hence LE p1,p2,P ; :: thesis: