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