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: now

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

end;

A11: P is being_simple_closed_curve by A1, JGRAPH_3:36;
then A12: Upper_Arc P is_an_arc_of W-min P, E-max P by JORDAN6:def 8;
set P4 = Lower_Arc P;
set P4b = Upper_Arc P;
A13: ( 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 A11, JORDAN6:def 9;
A14: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A1, Th37;
then A15: p1 in Upper_Arc P by A1;
A16: p2 in Upper_Arc P by A1, A14;
A17: W-min P = |[(- 1),0 ]| by A1, Th32;
A18: E-max P = |[1,0 ]| by A1, Th33;
for g being Function of I[01] ,((TOP-REAL 2) | (Upper_Arc P))
for s1, s2 being Real st g is being_homeomorphism & g . 0 = W-min P & g . 1 = E-max 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) | (Upper_Arc P)); :: thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = W-min P & g . 1 = E-max 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 = W-min P & g . 1 = E-max P & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume A19: ( g is being_homeomorphism & g . 0 = W-min P & g . 1 = E-max P & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 ) ; :: thesis: s1 <= s2
then A20: 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 = Upper_Arc P;
reconsider g2 = g0 | (Upper_Arc P) as Function of ((TOP-REAL 2) | (Upper_Arc P)),R^1 by PRE_TOPC:30;
reconsider g3 = g2 as continuous Function of ((TOP-REAL 2) | (Upper_Arc P)),(Closed-Interval-TSpace (- 1),1) by A1, Lm5;
E-max P in {(W-min P),(E-max P)} by TARSKI:def 2;
then A21: E-max P in Upper_Arc P by A13, XBOOLE_0:def 4;
W-min P in {(W-min P),(E-max P)} by TARSKI:def 2;
then A22: W-min P in Upper_Arc P by A13, XBOOLE_0:def 4;
A23: dom g3 = [#] ((TOP-REAL 2) | (Upper_Arc P)) by FUNCT_2:def 1;
A24: rng g3 = [#] (Closed-Interval-TSpace (- 1),1) by A1, Lm5;
A25: g3 is one-to-one by A1, Lm5;
( not Upper_Arc P is empty & Upper_Arc P is compact ) by A12, JORDAN5A:1;
then A26: (TOP-REAL 2) | (Upper_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 A27: g3 is being_homeomorphism by A23, A24, A25, A26, COMPTS_1:26;
reconsider h = g3 * g as Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace (- 1),1) by TOPMETR:27;
A28: h is being_homeomorphism by A19, A27, TOPMETR:27, TOPS_2:71;
A29: 0 in dom g by A20, XXREAL_1:1;
A30: 1 in dom g by A20, XXREAL_1:1;
A31: s1 in [.0 ,1.] by A19, XXREAL_1:1;
A32: s2 in [.0 ,1.] by A19, XXREAL_1:1;
A33: - 1 = |[(- 1),0 ]| `1 by EUCLID:56
.= proj1 . |[(- 1),0 ]| by PSCOMP_1:def 28
.= g3 . (g . 0 ) by A17, A19, A22, FUNCT_1:72
.= h . 0 by A29, FUNCT_1:23 ;
A34: 1 = |[1,0 ]| `1 by EUCLID:56
.= g0 . |[1,0 ]| by PSCOMP_1:def 28
.= g3 . |[1,0 ]| by A18, A21, FUNCT_1:72
.= h . 1 by A18, A19, A30, FUNCT_1:23 ;
A35: p1 `1 = g0 . p1 by PSCOMP_1:def 28
.= g3 . (g . s1) by A15, A19, FUNCT_1:72
.= h . s1 by A20, A31, FUNCT_1:23 ;
p2 `1 = g0 . p2 by PSCOMP_1:def 28
.= g3 . p2 by A16, FUNCT_1:72
.= h . s2 by A19, A20, A32, FUNCT_1:23 ;
hence s1 <= s2 by A1, A4, A28, A31, A32, A33, A34, A35, Th11; :: thesis: verum

end;

then ( p1 in Upper_Arc P & p2 in Upper_Arc P & LE p1,p2, Upper_Arc P, W-min P, E-max P ) by A15, A16, JORDAN5C:def 3;
hence LE p1,p2,P by JORDAN6:def 10; :: thesis: verum