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 & p1 <> W-min P 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 & p1 <> W-min P 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 & p1 <> W-min P )
; :: 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 & p1 <> W-min P )
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:
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) }
by A1, Th38;
now assume A6:
p1 in Upper_Arc P
;
:: thesis: p1 `1 > p2 `1
p1 in Lower_Arc P
by A3, A5;
then
p1 in {(W-min P),(E-max P)}
by A4, A6, XBOOLE_0:def 4;
then A7:
(
p1 = W-min P or
p1 = E-max P )
by TARSKI:def 2;
consider p9 being
Point of
(TOP-REAL 2) such that A8:
(
p9 = p2 &
|.p9.| = 1 )
by A3;
A9:
p1 = |[1,0 ]|
by A1, A7, Th33;
then A10:
p1 `1 = 1
by EUCLID:56;
p2 `1 <= 1
by A8, Th3;
hence
p1 `1 > p2 `1
by A10, A11, XXREAL_0:1;
:: thesis: verum end;
then A13:
( ( 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 ) or p1 `1 > p2 `1 )
by A1, JORDAN6:def 10;
consider f being Function of I[01] ,((TOP-REAL 2) | (Lower_Arc P)) such that
A14:
( 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;
A15: rng f =
[#] ((TOP-REAL 2) | (Lower_Arc P))
by A14, TOPS_2:def 5
.=
Lower_Arc P
by PRE_TOPC:def 10
;
now per cases
( not p1 `1 > p2 `1 or p1 `1 > p2 `1 )
;
case A16:
not
p1 `1 > p2 `1
;
:: thesis: p1 `1 > p2 `1 then consider x1 being
set such that A17:
(
x1 in dom f &
p1 = f . x1 )
by A13, A15, FUNCT_1:def 5;
consider x2 being
set such that A18:
(
x2 in dom f &
p2 = f . x2 )
by A13, A15, A16, FUNCT_1:def 5;
A19:
dom f =
[#] I[01]
by A14, TOPS_2:def 5
.=
[.0 ,1.]
by BORSUK_1:83
;
then reconsider r11 =
x1 as
Real by A17;
reconsider r22 =
x2 as
Real by A18, A19;
A20:
(
0 <= r11 &
r11 <= 1 )
by A17, A19, XXREAL_1:1;
A21:
(
0 <= r22 &
r22 <= 1 )
by A18, A19, XXREAL_1:1;
A22:
(
r11 < r22 iff
p1 `1 > p2 `1 )
by A14, A17, A18, A19;
(
r11 <= r22 or
p1 `1 > p2 `1 )
by A13, A14, A17, A18, A20, A21, JORDAN5C:def 3;
hence
p1 `1 > p2 `1
by A1, A17, A18, A22, XXREAL_0:1;
:: thesis: verum end;
hence
p1 `1 > p2 `1
; :: thesis: verum