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 } & p1 in P & p2 in P & p1 `1 >= 0 & p2 `1 >= 0 & p1 `2 >= p2 `2 holds
LE p1,p2,P
let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p1 `1 >= 0 & p2 `1 >= 0 & p1 `2 >= p2 `2 implies LE p1,p2,P )
assume A1: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p1 `1 >= 0 & p2 `1 >= 0 & p1 `2 >= p2 `2 ) ; :: thesis: LE p1,p2,P
then consider p3 being Point of (TOP-REAL 2) such that
A2: ( p3 = p1 & |.p3.| = 1 ) ;
consider p3 being Point of (TOP-REAL 2) such that
A3: ( p3 = p2 & |.p3.| = 1 ) by A1;
A4: P is being_simple_closed_curve by A1, JGRAPH_3:36;
then A5: Lower_Arc P is_an_arc_of E-max P, W-min P by JORDAN6:def 9;
set P4b = Lower_Arc P;
A6: ( 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 A4, JORDAN6:def 9;
A7: Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A1, Th37;
A8: W-min P = |[(- 1),0 ]| by A1, Th32;
A9: E-max P = |[1,0 ]| by A1, Th33;
now
per cases ( ( p1 in Upper_Arc P & p2 in Upper_Arc P ) or ( p1 in Upper_Arc P & not p2 in Upper_Arc P ) or ( not p1 in Upper_Arc P & p2 in Upper_Arc P ) or ( not p1 in Upper_Arc P & not p2 in Upper_Arc P ) ) ;
case ( p1 in Upper_Arc P & p2 in Upper_Arc P ) ; :: thesis: LE p1,p2,P
then consider p22 being Point of (TOP-REAL 2) such that
A10: ( p2 = p22 & p22 in P & p22 `2 >= 0 ) by A7;
(p1 `2 ) ^2 >= (p2 `2 ) ^2 by A1, A10, SQUARE_1:77;
then A11: (1 ^2 ) - ((p1 `2 ) ^2 ) <= (1 ^2 ) - ((p2 `2 ) ^2 ) by XREAL_1:15;
A12: 1 ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) by A2, JGRAPH_3:10;
then A13: p1 `1 = sqrt ((1 ^2 ) - ((p1 `2 ) ^2 )) by A1, SQUARE_1:89;
1 ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) by A3, JGRAPH_3:10;
then A14: p2 `1 = sqrt ((1 ^2 ) - ((p2 `2 ) ^2 )) by A1, SQUARE_1:89;
(1 ^2 ) - ((p1 `2 ) ^2 ) >= 0 by A12, XREAL_1:65;
hence LE p1,p2,P by A1, A10, A11, A13, A14, Th57, SQUARE_1:94; :: thesis: verum
end;
case A18: ( not p1 in Upper_Arc P & p2 in Upper_Arc P ) ; :: thesis: contradiction
then consider p9 being Point of (TOP-REAL 2) such that
A19: ( p2 = p9 & p9 in P & p9 `2 >= 0 ) by A7;
thus contradiction by A1, A7, A18, A19; :: thesis: verum
end;
case A20: ( not p1 in Upper_Arc P & not p2 in Upper_Arc P ) ; :: thesis: LE p1,p2,P
then A21: p1 in Lower_Arc P by A1, A6, XBOOLE_0:def 3;
A22: p2 in Lower_Arc P by A1, A6, A20, XBOOLE_0:def 3;
p1 `2 < 0 by A1, A7, A20;
then A23: - (p1 `2 ) > 0 by XREAL_1:60;
- (p1 `2 ) <= - (p2 `2 ) by A1, XREAL_1:26;
then (- (p1 `2 )) ^2 <= (- (p2 `2 )) ^2 by A23, SQUARE_1:77;
then A24: (1 ^2 ) - ((- (p1 `2 )) ^2 ) >= (1 ^2 ) - ((- (p2 `2 )) ^2 ) by XREAL_1:15;
1 ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) by A2, JGRAPH_3:10;
then A25: p1 `1 = sqrt ((1 ^2 ) - ((- (p1 `2 )) ^2 )) by A1, SQUARE_1:89;
A26: 1 ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) by A3, JGRAPH_3:10;
then A27: p2 `1 = sqrt ((1 ^2 ) - ((- (p2 `2 )) ^2 )) by A1, SQUARE_1:89;
(1 ^2 ) - ((- (p2 `2 )) ^2 ) >= 0 by A26, XREAL_1:65;
then A28: p1 `1 >= p2 `1 by A24, A25, A27, SQUARE_1:94;
A29: for g being Function of I[01] ,((TOP-REAL 2) | (Lower_Arc P))
for s1, s2 being Real st g is being_homeomorphism & g . 0 = E-max P & g . 1 = W-min P & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2
proof
let g be Function of I[01] ,((TOP-REAL 2) | (Lower_Arc P)); :: thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = E-max P & g . 1 = W-min P & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2
let s1, s2 be Real; :: thesis: ( g is being_homeomorphism & g . 0 = E-max P & g . 1 = W-min P & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume A30: ( g is being_homeomorphism & g . 0 = E-max P & g . 1 = W-min P & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 ) ; :: thesis: s1 <= s2
then A31: dom g = [#] I[01] by TOPS_2:def 5
.= [.0 ,1.] by BORSUK_1:83 ;
reconsider g0 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
set K0 = Lower_Arc P;
reconsider g2 = g0 | (Lower_Arc P) as Function of ((TOP-REAL 2) | (Lower_Arc P)),R^1 by PRE_TOPC:30;
reconsider g3 = g2 as continuous Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace (- 1),1) by A1, Lm4;
E-max P in {(W-min P),(E-max P)} by TARSKI:def 2;
then A32: E-max P in Lower_Arc P by A6, XBOOLE_0:def 4;
W-min P in {(W-min P),(E-max P)} by TARSKI:def 2;
then A33: W-min P in Lower_Arc P by A6, XBOOLE_0:def 4;
A34: dom g3 = [#] ((TOP-REAL 2) | (Lower_Arc P)) by FUNCT_2:def 1;
A35: rng g3 = [#] (Closed-Interval-TSpace (- 1),1) by A1, Lm4;
A36: g3 is one-to-one by A1, Lm4;
( not Lower_Arc P is empty & Lower_Arc P is compact ) by A5, JORDAN5A:1;
then A37: (TOP-REAL 2) | (Lower_Arc P) is compact ;
Closed-Interval-TSpace (- 1),1 = TopSpaceMetr (Closed-Interval-MSpace (- 1),1) by TOPMETR:def 8;
then Closed-Interval-TSpace (- 1),1 is T_2 by PCOMPS_1:38;
then A38: g3 is being_homeomorphism by A34, A35, A36, A37, COMPTS_1:26;
reconsider h = g3 * g as Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace (- 1),1) by TOPMETR:27;
A39: h is being_homeomorphism by A30, A38, TOPMETR:27, TOPS_2:71;
A40: 0 in dom g by A31, XXREAL_1:1;
A41: 1 in dom g by A31, XXREAL_1:1;
A42: s1 in [.0 ,1.] by A30, XXREAL_1:1;
A43: s2 in [.0 ,1.] by A30, XXREAL_1:1;
A44: - 1 = |[(- 1),0 ]| `1 by EUCLID:56
.= proj1 . |[(- 1),0 ]| by PSCOMP_1:def 28
.= g3 . |[(- 1),0 ]| by A8, A33, FUNCT_1:72
.= h . 1 by A8, A30, A41, FUNCT_1:23 ;
A45: 1 = |[1,0 ]| `1 by EUCLID:56
.= proj1 . |[1,0 ]| by PSCOMP_1:def 28
.= g3 . |[1,0 ]| by A9, A32, FUNCT_1:72
.= h . 0 by A9, A30, A40, FUNCT_1:23 ;
A46: p1 `1 = g0 . p1 by PSCOMP_1:def 28
.= g3 . p1 by A21, FUNCT_1:72
.= h . s1 by A30, A31, A42, FUNCT_1:23 ;
p2 `1 = g0 . p2 by PSCOMP_1:def 28
.= g3 . p2 by A22, FUNCT_1:72
.= h . s2 by A30, A31, A43, FUNCT_1:23 ;
hence s1 <= s2 by A28, A39, A42, A43, A44, A45, A46, Th12; :: thesis: verum
end;
A47: now
assume A48: p2 = W-min P ; :: thesis: contradiction
W-min P = |[(- 1),0 ]| by A1, Th32;
then p2 `2 = 0 by A48, EUCLID:56;
hence contradiction by A1, A7, A20; :: thesis: verum
end;
( p1 in Lower_Arc P & p2 in Lower_Arc P & LE p1,p2, Lower_Arc P, E-max P, W-min P ) by A21, A22, A29, JORDAN5C:def 3;
hence LE p1,p2,P by A47, JORDAN6:def 10; :: thesis: verum
end;
end;
end;
hence LE p1,p2,P ; :: thesis: verum