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

A6: now

assume p2 = W-min P ; :: thesis: contradiction
then LE p2,p1,P by A2, A3, JORDAN7:3;
hence contradiction by A1, JGRAPH_3:36, JORDAN6:72; :: thesis: verum

end;

now

assume A7: p2 in Lower_Arc P ; :: thesis: p1 `1 < p2 `1
p2 in Upper_Arc P by A3, A5;
then p2 in {(W-min P),(E-max P)} by A4, A7, XBOOLE_0:def 4;
then A8: ( p2 = W-min P or p2 = E-max P ) by TARSKI:def 2;
consider p8 being Point of (TOP-REAL 2) such that
A9: ( p8 = p1 & |.p8.| = 1 ) by A3;

now

assume p2 = W-min P ; :: thesis: contradiction
then LE p2,p1,P by A2, A3, JORDAN7:3;
hence contradiction by A1, JGRAPH_3:36, JORDAN6:72; :: thesis: verum

end;

then A10: p2 = |[1,0 ]| by A1, A8, Th33;
then A11: p2 `1 = 1 by EUCLID:56;

A12: now

assume A13: p1 `1 = 1 ; :: thesis: contradiction
1 ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) by A9, JGRAPH_3:10;
then p1 `2 = 0 by A13, XCMPLX_1:6;
hence contradiction by A1, A10, A13, EUCLID:57; :: thesis: verum

end;

p1 `1 <= 1 by A9, Th3;
hence p1 `1 < p2 `1 by A11, A12, XXREAL_0:1; :: thesis: verum

end;

then A14: ( ( p1 in Upper_Arc P & p2 in Upper_Arc P & not p2 = W-min P & LE p1,p2, Upper_Arc P, W-min P, E-max P ) or p1 `1 < p2 `1 ) by A1, A6, JORDAN6:def 10;
consider f being Function of I[01] ,((TOP-REAL 2) | (Upper_Arc P)) such that
A15: ( 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 = W-min P & f . 1 = E-max P ) by A1, Th46;
A16: rng f = [#] ((TOP-REAL 2) | (Upper_Arc P)) by A15, TOPS_2:def 5
.= Upper_Arc P by PRE_TOPC:def 10 ;

now

per cases ( not p1 `1 < p2 `1 or p1 `1 < p2 `1 ) ;

case A17: not p1 `1 < p2 `1 ; :: thesis: p1 `1 < p2 `1

then consider x1 being set such that
A18: ( x1 in dom f & p1 = f . x1 ) by A14, A16, FUNCT_1:def 5;
consider x2 being set such that
A19: ( x2 in dom f & p2 = f . x2 ) by A14, A16, A17, FUNCT_1:def 5;
A20: dom f = [#] I[01] by A15, TOPS_2:def 5
.= [.0 ,1.] by BORSUK_1:83 ;
then reconsider r11 = x1 as Real by A18;
reconsider r22 = x2 as Real by A19, A20;
A21: ( 0 <= r11 & r11 <= 1 ) by A18, A20, XXREAL_1:1;
A22: ( 0 <= r22 & r22 <= 1 ) by A19, A20, XXREAL_1:1;
A23: ( r11 < r22 iff p1 `1 < p2 `1 ) by A15, A18, A19, A20;
( r11 <= r22 or p1 `1 < p2 `1 ) by A14, A15, A18, A19, A21, A22, JORDAN5C:def 3;
hence p1 `1 < p2 `1 by A1, A18, A19, A23, XXREAL_0:1; :: thesis: verum

end;

case p1 `1 < p2 `1 ; :: thesis: p1 `1 < p2 `1

hence p1 `1 < p2 `1 ; :: thesis: verum

end;

end;

end;

hence p1 `1 < p2 `1 ; :: thesis: verum