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 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: LE p1,p2,P
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: - (p1 `2 ) > 0 by A1, XREAL_1:60;

A5: now

assume p1 `2 >= p2 `2 ; :: thesis: p1 `1 >= p2 `1
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;
1 ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) by A2, JGRAPH_3:10;
then A7: p1 `1 = sqrt ((1 ^2 ) - ((- (p1 `2 )) ^2 )) by A1, SQUARE_1:89;
A8: 1 ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) by A3, JGRAPH_3:10;
then A9: p2 `1 = sqrt ((1 ^2 ) - ((- (p2 `2 )) ^2 )) by A1, SQUARE_1:89;
(1 ^2 ) - ((- (p2 `2 )) ^2 ) >= 0 by A8, XREAL_1:65;
hence p1 `1 >= p2 `1 by A6, A7, A9, SQUARE_1:94; :: thesis: verum

end;

A10: P is being_simple_closed_curve by A1, JGRAPH_3:36;
then A11: Lower_Arc P is_an_arc_of E-max P, W-min P by JORDAN6:def 9;
set P4 = Lower_Arc P;
A12: ( 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 A10, JORDAN6:def 9;
A13: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A1, Th37;

A14: now

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

end;

A16: now

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

end;

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

A20: now

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

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: 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 A22: ( 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: s1 <= s2
then A23: 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 A24: E-max P in Lower_Arc P by A12, XBOOLE_0:def 4;
W-min P in {(W-min P),(E-max P)} by TARSKI:def 2;
then A25: W-min P in Lower_Arc P by A12, XBOOLE_0:def 4;
A26: dom g3 = [#] ((TOP-REAL 2) | (Lower_Arc P)) by FUNCT_2:def 1;
A27: rng g3 = [#] (Closed-Interval-TSpace (- 1),1) by A1, Lm4;
A28: g3 is one-to-one by A1, Lm4;
( not Lower_Arc P is empty & Lower_Arc P is compact ) by A11, JORDAN5A:1;
then A29: (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 A30: g3 is being_homeomorphism by A26, A27, A28, A29, COMPTS_1:26;
reconsider h = g3 * g as Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace (- 1),1) by TOPMETR:27;
A31: h is being_homeomorphism by A22, A30, TOPMETR:27, TOPS_2:71;
A32: 0 in dom g by A23, XXREAL_1:1;
A33: 1 in dom g by A23, XXREAL_1:1;
A34: s1 in [.0 ,1.] by A22, XXREAL_1:1;
A35: s2 in [.0 ,1.] by A22, XXREAL_1:1;
A36: - 1 = |[(- 1),0 ]| `1 by EUCLID:56
.= proj1 . |[(- 1),0 ]| by PSCOMP_1:def 28
.= g3 . (g . 1) by A18, A22, A25, FUNCT_1:72
.= h . 1 by A33, FUNCT_1:23 ;
A37: 1 = |[1,0 ]| `1 by EUCLID:56
.= proj1 . |[1,0 ]| by PSCOMP_1:def 28
.= g3 . (g . 0 ) by A19, A22, A24, FUNCT_1:72
.= h . 0 by A32, FUNCT_1:23 ;
A38: p1 `1 = g0 . p1 by PSCOMP_1:def 28
.= g3 . (g . s1) by A14, A22, FUNCT_1:72
.= h . s1 by A23, A34, FUNCT_1:23 ;
p2 `1 = proj1 . p2 by PSCOMP_1:def 28
.= g3 . p2 by A16, FUNCT_1:72
.= h . s2 by A22, A23, A35, FUNCT_1:23 ;
hence s1 <= s2 by A1, A5, A31, A34, A35, A36, A37, A38, Th12; :: thesis: verum

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 A14, A16, A20, JORDAN5C:def 3;
hence LE p1,p2,P by JORDAN6:def 10; :: thesis: verum