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 & p2 `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 & p2 `1 < 0 & p1 `2 < 0 & p2 `2 < 0 implies ( p1 `1 > p2 `1 & p1 `2 < p2 `2 ) )
assume A1: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & p1 <> p2 & p1 `1 < 0 & p2 `1 < 0 & p1 `2 < 0 & p2 `2 < 0 ) ; :: thesis: ( p1 `1 > p2 `1 & p1 `2 < p2 `2 )
then P is being_simple_closed_curve by JGRAPH_3:36;
then A2: ( p1 in P & p2 in P ) by A1, JORDAN7:5;
A3: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A1, Th37;

now

assume p1 in Upper_Arc P ; :: thesis: contradiction
then consider p being Point of (TOP-REAL 2) such that
A4: ( p1 = p & p in P & p `2 >= 0 ) by A3;
thus contradiction by A1, A4; :: thesis: verum

end;

then A5: ( 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 A1, JORDAN6:def 10;
consider f being Function of I[01] ,((TOP-REAL 2) | (Lower_Arc P)) such that
A6: ( f is being_homeomorphism & ( 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 ) ) & f . 0 = E-max P & f . 1 = W-min P ) by A1, Th45;
A7: rng f = [#] ((TOP-REAL 2) | (Lower_Arc P)) by A6, TOPS_2:def 5
.= Lower_Arc P by PRE_TOPC:def 10 ;
then consider x1 being set such that
A8: ( x1 in dom f & p1 = f . x1 ) by A5, FUNCT_1:def 5;
consider x2 being set such that
A9: ( x2 in dom f & p2 = f . x2 ) by A5, A7, FUNCT_1:def 5;
A10: dom f = [#] I[01] by A6, TOPS_2:def 5
.= [.0 ,1.] by BORSUK_1:83 ;
then reconsider r11 = x1 as Real by A8;
reconsider r22 = x2 as Real by A9, A10;
A11: ( 0 <= r11 & r11 <= 1 ) by A8, A10, XXREAL_1:1;
A12: ( 0 <= r22 & r22 <= 1 ) by A9, A10, XXREAL_1:1;
A13: ( r11 < r22 iff p1 `1 > p2 `1 ) by A6, A8, A9, A10;
A14: r11 <= r22 by A5, A6, A8, A9, A11, A12, JORDAN5C:def 3;
consider p3 being Point of (TOP-REAL 2) such that
A15: ( p3 = p1 & |.p3.| = 1 ) by A1, A2;
1 ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) by A15, JGRAPH_3:10;
then A16: (1 ^2 ) - ((p1 `1 ) ^2 ) = (- (p1 `2 )) ^2 ;
A17: - (p1 `1 ) > 0 by A1, XREAL_1:60;
- (p1 `2 ) > 0 by A1, XREAL_1:60;
then - (p1 `2 ) = sqrt ((1 ^2 ) - ((- (p1 `1 )) ^2 )) by A16, SQUARE_1:89;
then A18: p1 `2 = - (sqrt ((1 ^2 ) - ((- (p1 `1 )) ^2 ))) ;
consider p4 being Point of (TOP-REAL 2) such that
A19: ( p4 = p2 & |.p4.| = 1 ) by A1, A2;
A20: 1 ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) by A19, JGRAPH_3:10;
then A21: (1 ^2 ) - ((p2 `1 ) ^2 ) = (- (p2 `2 )) ^2 ;
- (p2 `2 ) > 0 by A1, XREAL_1:60;
then - (p2 `2 ) = sqrt ((1 ^2 ) - ((- (p2 `1 )) ^2 )) by A21, SQUARE_1:89;
then A22: p2 `2 = - (sqrt ((1 ^2 ) - ((- (p2 `1 )) ^2 ))) ;
- (p1 `1 ) < - (p2 `1 ) by A1, A8, A9, A13, A14, XREAL_1:26, XXREAL_0:1;
then (- (p1 `1 )) ^2 < (- (p2 `1 )) ^2 by A17, SQUARE_1:78;
then (1 ^2 ) - ((- (p1 `1 )) ^2 ) > (1 ^2 ) - ((- (p2 `1 )) ^2 ) by XREAL_1:17;
then sqrt ((1 ^2 ) - ((- (p1 `1 )) ^2 )) > sqrt ((1 ^2 ) - ((- (p2 `1 )) ^2 )) by A20, SQUARE_1:95, XREAL_1:65;
hence ( p1 `1 > p2 `1 & p1 `2 < p2 `2 ) by A8, A9, A13, A14, A18, A22, XREAL_1:26, XXREAL_0:1; :: thesis: verum