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 `2 >= 0 & p2 `2 >= 0 & p1 `1 <= p2 `1 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 `2 >= 0 & p2 `2 >= 0 & p1 `1 <= p2 `1 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 `2 >= 0 & p2 `2 >= 0 & p1 `1 <= p2 `1 )
; :: thesis: LE p1,p2,P
then A2:
P is being_simple_closed_curve
by JGRAPH_3:36;
then A3:
Upper_Arc P is_an_arc_of W-min P, E-max P
by JORDAN6:def 8;
set P4 = Lower_Arc P;
set P4b = Upper_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 A6:
p1 in Upper_Arc P
by A1;
A7:
p2 in Upper_Arc P
by A1, A5;
A8:
W-min P = |[(- 1),0 ]|
by A1, Th32;
A9:
E-max P = |[1,0 ]|
by A1, Th33;
for g being Function of I[01] ,((TOP-REAL 2) | (Upper_Arc P))
for s1, s2 being Real st g is being_homeomorphism & g . 0 = W-min P & g . 1 = E-max 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) | (Upper_Arc P));
:: thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = W-min P & g . 1 = E-max P & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2let s1,
s2 be
Real;
:: thesis: ( g is being_homeomorphism & g . 0 = W-min P & g . 1 = E-max P & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume A10:
(
g is
being_homeomorphism &
g . 0 = W-min P &
g . 1
= E-max P &
g . s1 = p1 &
0 <= s1 &
s1 <= 1 &
g . s2 = p2 &
0 <= s2 &
s2 <= 1 )
;
:: thesis: s1 <= s2
then A11:
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 =
Upper_Arc P;
reconsider g2 =
g0 | (Upper_Arc P) as
Function of
((TOP-REAL 2) | (Upper_Arc P)),
R^1 by PRE_TOPC:30;
reconsider g3 =
g2 as
continuous Function of
((TOP-REAL 2) | (Upper_Arc P)),
(Closed-Interval-TSpace (- 1),1) by A1, Lm5;
E-max P in {(W-min P),(E-max P)}
by TARSKI:def 2;
then A12:
E-max P in Upper_Arc P
by A4, XBOOLE_0:def 4;
W-min P in {(W-min P),(E-max P)}
by TARSKI:def 2;
then A13:
W-min P in Upper_Arc P
by A4, XBOOLE_0:def 4;
A14:
dom g3 = [#] ((TOP-REAL 2) | (Upper_Arc P))
by FUNCT_2:def 1;
A15:
rng g3 = [#] (Closed-Interval-TSpace (- 1),1)
by A1, Lm5;
A16:
g3 is
one-to-one
by A1, Lm5;
( not
Upper_Arc P is
empty &
Upper_Arc P is
compact )
by A3, JORDAN5A:1;
then A17:
(TOP-REAL 2) | (Upper_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 A18:
g3 is
being_homeomorphism
by A14, A15, A16, A17, COMPTS_1:26;
reconsider h =
g3 * g as
Function of
(Closed-Interval-TSpace 0 ,1),
(Closed-Interval-TSpace (- 1),1) by TOPMETR:27;
A19:
h is
being_homeomorphism
by A10, A18, TOPMETR:27, TOPS_2:71;
A20:
0 in dom g
by A11, XXREAL_1:1;
A21:
1
in dom g
by A11, XXREAL_1:1;
A22:
s1 in [.0 ,1.]
by A10, XXREAL_1:1;
A23:
s2 in [.0 ,1.]
by A10, XXREAL_1:1;
A24:
- 1 =
|[(- 1),0 ]| `1
by EUCLID:56
.=
proj1 . |[(- 1),0 ]|
by PSCOMP_1:def 28
.=
g3 . |[(- 1),0 ]|
by A8, A13, FUNCT_1:72
.=
h . 0
by A8, A10, A20, FUNCT_1:23
;
A25: 1 =
|[1,0 ]| `1
by EUCLID:56
.=
g0 . |[1,0 ]|
by PSCOMP_1:def 28
.=
g3 . |[1,0 ]|
by A9, A12, FUNCT_1:72
.=
h . 1
by A9, A10, A21, FUNCT_1:23
;
A26:
p1 `1 =
g0 . p1
by PSCOMP_1:def 28
.=
g3 . p1
by A6, FUNCT_1:72
.=
h . s1
by A10, A11, A22, FUNCT_1:23
;
p2 `1 =
g0 . p2
by PSCOMP_1:def 28
.=
g3 . p2
by A7, FUNCT_1:72
.=
h . s2
by A10, A11, A23, FUNCT_1:23
;
hence
s1 <= s2
by A1, A19, A22, A23, A24, A25, A26, Th11;
:: thesis: verum
end;
then
( p1 in Upper_Arc P & p2 in Upper_Arc P & LE p1,p2, Upper_Arc P, W-min P, E-max P )
by A6, A7, JORDAN5C:def 3;
hence
LE p1,p2,P
by JORDAN6:def 10; :: thesis: verum