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 holds
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 implies 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: p2 `1 >= 0 ; :: thesis: p1 `2 > p2 `2
A6: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A1, Th34;
A7: P is being_simple_closed_curve by A1, JGRAPH_3:26;
then A8: p2 in P by A2, JORDAN7:5;
then A9: ex p3 being Point of (TOP-REAL 2) st
( p3 = p2 & |.p3.| = 1 ) by A1;
W-min P = |[(- 1),0]| by A1, Th29;
then A10: (W-min P) `2 = 0 by EUCLID:52;
A11: Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A1, Th35;
A12: p1 in P by A2, A7, JORDAN7:5;
then A13: ex p4 being Point of (TOP-REAL 2) st
( p4 = p1 & |.p4.| = 1 ) by A1;
now :: thesis: ( ( p1 `2 >= 0 & p2 `2 >= 0 & p1 `2 > p2 `2 ) or ( p1 `2 >= 0 & p2 `2 < 0 & p1 `2 > p2 `2 ) or ( p1 `2 < 0 & p2 `2 >= 0 & contradiction ) or ( p1 `2 < 0 & p2 `2 < 0 & p1 `2 > p2 `2 ) )
per cases ( ( p1 `2 >= 0 & p2 `2 >= 0 ) or ( p1 `2 >= 0 & p2 `2 < 0 ) or ( p1 `2 < 0 & p2 `2 >= 0 ) or ( p1 `2 < 0 & p2 `2 < 0 ) ) ;
case A14: ( p1 `2 >= 0 & p2 `2 >= 0 ) ; :: thesis: p1 `2 > p2 `2
then p1 `1 < p2 `1 by A1, A2, A3, Th47;
then (p1 `1) ^2 < (p2 `1) ^2 by A4, SQUARE_1:16;
then A15: (1 ^2) - ((p1 `1) ^2) > (1 ^2) - ((p2 `1) ^2) by XREAL_1:15;
1 ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by A13, JGRAPH_3:1;
then A16: p1 `2 = sqrt ((1 ^2) - ((p1 `1) ^2)) by A14, SQUARE_1:22;
A17: 1 ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by A9, JGRAPH_3:1;
then p2 `2 = sqrt ((1 ^2) - ((p2 `1) ^2)) by A14, SQUARE_1:22;
hence p1 `2 > p2 `2 by A15, A16, A17, SQUARE_1:27, XREAL_1:63; :: thesis: verum
end;
case ( p1 `2 >= 0 & p2 `2 < 0 ) ; :: thesis: p1 `2 > p2 `2
hence p1 `2 > p2 `2 ; :: thesis: verum
end;
case A19: ( p1 `2 < 0 & p2 `2 < 0 ) ; :: thesis: p1 `2 > p2 `2
ex p3 being Point of (TOP-REAL 2) st
( p3 = p1 & |.p3.| = 1 ) by A1, A12;
then A20: 1 ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by JGRAPH_3:1;
then (1 ^2) - ((p1 `1) ^2) = (- (p1 `2)) ^2 ;
then A21: - (p1 `2) = sqrt ((1 ^2) - ((p1 `1) ^2)) by A19, SQUARE_1:22;
for p being Point of (TOP-REAL 2) holds
( not p = p1 or not p in P or not p `2 >= 0 ) by A19;
then A22: not p1 in Upper_Arc P by A6;
then A23: LE p1,p2, Lower_Arc P, E-max P, W-min P by A2;
ex p4 being Point of (TOP-REAL 2) st
( p4 = p2 & |.p4.| = 1 ) by A1, A8;
then 1 ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by JGRAPH_3:1;
then (1 ^2) - ((p2 `1) ^2) = (- (p2 `2)) ^2 ;
then A24: - (p2 `2) = sqrt ((1 ^2) - ((p2 `1) ^2)) by A19, SQUARE_1:22;
consider f being Function of I[01],((TOP-REAL 2) | (Lower_Arc P)) such that
A25: f is being_homeomorphism and
A26: 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
A27: ( f . 0 = E-max P & f . 1 = W-min P ) by A1, Th42;
A28: rng f = [#] ((TOP-REAL 2) | (Lower_Arc P)) by A25, TOPS_2:def 5
.= Lower_Arc P by PRE_TOPC:def 5 ;
p2 in Lower_Arc P by A2, A22;
then consider x2 being object such that
A29: x2 in dom f and
A30: p2 = f . x2 by A28, FUNCT_1:def 3;
A31: dom f = [#] I[01] by A25, TOPS_2:def 5
.= [.0,1.] by BORSUK_1:40 ;
reconsider r22 = x2 as Real by A29;
A32: ( 0 <= r22 & r22 <= 1 ) by A29, A31, XXREAL_1:1;
p1 in Lower_Arc P by A2, A22;
then consider x1 being object such that
A33: x1 in dom f and
A34: p1 = f . x1 by A28, FUNCT_1:def 3;
reconsider r11 = x1 as Real by A33;
A35: ( r11 < r22 iff p1 `1 > p2 `1 ) by A26, A33, A34, A29, A30, A31;
r11 <= 1 by A33, A31, XXREAL_1:1;
then r11 <= r22 by A23, A25, A27, A34, A30, A32, JORDAN5C:def 3;
then (p1 `1) ^2 > (p2 `1) ^2 by A3, A5, A34, A30, A35, SQUARE_1:16, XXREAL_0:1;
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 A20, SQUARE_1:27, XREAL_1:63;
hence p1 `2 > p2 `2 by A21, A24, XREAL_1:24; :: thesis: verum
end;
end;
end;
hence p1 `2 > p2 `2 ; :: thesis: verum