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 } & LE p1,p2,P & p1 <> p2 & p1 `1 < 0 & p1 `2 < 0 & p2 `2 < 0 holds
( p1 `1 > p2 `1 & p1 `2 < p2 `2 )
let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & p1 <> p2 & p1 `1 < 0 & p1 `2 < 0 & p2 `2 < 0 implies ( p1 `1 > p2 `1 & p1 `2 < p2 `2 ) )
assume that
A1: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } and
A2: LE p1,p2,P and
A3: p1 <> p2 and
A4: p1 `1 < 0 and
A5: p1 `2 < 0 and
A6: p2 `2 < 0 ; :: thesis: ( p1 `1 > p2 `1 & p1 `2 < p2 `2 )
consider f being Function of I[01],((TOP-REAL 2) | (Lower_Arc P)) such that
A7: f is being_homeomorphism and
A8: for q1, q2 being Point of (TOP-REAL 2)
for r1, r2 being Real st f . r1 = q1 & f . r2 = q2 & r1 in [.0,1.] & r2 in [.0,1.] holds
( r1 < r2 iff q1 `1 > q2 `1 ) and
A9: ( f . 0 = E-max P & f . 1 = W-min P ) by A1, Th42;
A10: rng f = [#] ((TOP-REAL 2) | (Lower_Arc P)) by A7, TOPS_2:def 5
.= Lower_Arc P by PRE_TOPC:def 5 ;
A11: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A1, Th34;

A12: now :: thesis: not p1 in Upper_Arc P

assume p1 in Upper_Arc P ; :: thesis: contradiction
then ex p being Point of (TOP-REAL 2) st
( p1 = p & p in P & p `2 >= 0 ) by A11;
hence contradiction by A5; :: thesis: verum

end;

then A13: LE p1,p2, Lower_Arc P, E-max P, W-min P by A2;
p2 in Lower_Arc P by A2, A12;
then consider x2 being object such that
A14: x2 in dom f and
A15: p2 = f . x2 by A10, FUNCT_1:def 3;
A16: dom f = [#] I[01] by A7, TOPS_2:def 5
.= [.0,1.] by BORSUK_1:40 ;
reconsider r22 = x2 as Real by A14;
A17: ( 0 <= r22 & r22 <= 1 ) by A14, A16, XXREAL_1:1;
p1 in Lower_Arc P by A2, A12;
then consider x1 being object such that
A18: x1 in dom f and
A19: p1 = f . x1 by A10, FUNCT_1:def 3;
reconsider r11 = x1 as Real by A18;
r11 <= 1 by A18, A16, XXREAL_1:1;
then A20: r11 <= r22 by A13, A7, A9, A19, A15, A17, JORDAN5C:def 3;
A21: P is being_simple_closed_curve by A1, JGRAPH_3:26;
then p1 in P by A2, JORDAN7:5;
then ex p3 being Point of (TOP-REAL 2) st
( p3 = p1 & |.p3.| = 1 ) by A1;
then 1 ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by JGRAPH_3:1;
then (1 ^2) - ((p1 `1) ^2) = (- (p1 `2)) ^2 ;
then - (p1 `2) = sqrt ((1 ^2) - ((- (p1 `1)) ^2)) by A5, SQUARE_1:22;
then A22: p1 `2 = - (sqrt ((1 ^2) - ((- (p1 `1)) ^2))) ;
p2 in P by A2, A21, JORDAN7:5;
then ex p4 being Point of (TOP-REAL 2) st
( p4 = p2 & |.p4.| = 1 ) by A1;
then A23: 1 ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by JGRAPH_3:1;
then (1 ^2) - ((p2 `1) ^2) = (- (p2 `2)) ^2 ;
then - (p2 `2) = sqrt ((1 ^2) - ((- (p2 `1)) ^2)) by A6, SQUARE_1:22;
then A24: p2 `2 = - (sqrt ((1 ^2) - ((- (p2 `1)) ^2))) ;
A25: ( r11 < r22 iff p1 `1 > p2 `1 ) by A8, A18, A19, A14, A15, A16;
then - (p1 `1) < - (p2 `1) by A3, A19, A15, A20, XREAL_1:24, XXREAL_0:1;
then (- (p1 `1)) ^2 < (- (p2 `1)) ^2 by A4, SQUARE_1:16;
then (1 ^2) - ((- (p1 `1)) ^2) > (1 ^2) - ((- (p2 `1)) ^2) by XREAL_1:15;
then sqrt ((1 ^2) - ((- (p1 `1)) ^2)) > sqrt ((1 ^2) - ((- (p2 `1)) ^2)) by A23, SQUARE_1:27, XREAL_1:63;
hence ( p1 `1 > p2 `1 & p1 `2 < p2 `2 ) by A19, A15, A25, A20, A22, A24, XREAL_1:24, XXREAL_0:1; :: thesis: verum