let p1, p2 be Point of (TOP-REAL 2); 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); ( 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 that
A1:
P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 }
and
A2:
p1 in P
and
A3:
p2 in P
and
A4:
p1 `2 >= 0
and
A5:
p2 `2 >= 0
and
A6:
p1 `1 <= p2 `1
; LE p1,p2,P
A7:
Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
by A1, Th34;
then A8:
p1 in Upper_Arc P
by A2, A4;
A9:
p2 in Upper_Arc P
by A3, A5, A7;
set P4b = Upper_Arc P;
set P4 = Lower_Arc P;
A10:
P is being_simple_closed_curve
by A1, JGRAPH_3:26;
then A11:
(Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)}
by JORDAN6:def 9;
A12:
E-max P = |[1,0]|
by A1, Th30;
A13:
Upper_Arc P is_an_arc_of W-min P, E-max P
by A10, JORDAN6:def 8;
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
E-max P in {(W-min P),(E-max P)}
by TARSKI:def 2;
then A14:
E-max P in Upper_Arc P
by A11, XBOOLE_0:def 4;
set K0 =
Upper_Arc P;
reconsider g0 =
proj1 as
Function of
(TOP-REAL 2),
R^1 by TOPMETR:17;
reconsider g2 =
g0 | (Upper_Arc P) as
Function of
((TOP-REAL 2) | (Upper_Arc P)),
R^1 by PRE_TOPC:9;
Closed-Interval-TSpace (
(- 1),1)
= TopSpaceMetr (Closed-Interval-MSpace ((- 1),1))
by TOPMETR:def 7;
then A15:
Closed-Interval-TSpace (
(- 1),1) is
T_2
by PCOMPS_1:34;
reconsider g3 =
g2 as
continuous Function of
((TOP-REAL 2) | (Upper_Arc P)),
(Closed-Interval-TSpace ((- 1),1)) by A1, Lm6;
let g be
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 <= s2let s1,
s2 be
Real;
( 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 that A16:
g is
being_homeomorphism
and
g . 0 = W-min P
and A17:
g . 1
= E-max P
and A18:
g . s1 = p1
and A19:
(
0 <= s1 &
s1 <= 1 )
and A20:
g . s2 = p2
and A21:
(
0 <= s2 &
s2 <= 1 )
;
s1 <= s2
A22:
s2 in [.0,1.]
by A21, XXREAL_1:1;
reconsider h =
g3 * g as
Function of
(Closed-Interval-TSpace (0,1)),
(Closed-Interval-TSpace ((- 1),1)) by TOPMETR:20;
A23:
(
dom g3 = [#] ((TOP-REAL 2) | (Upper_Arc P)) &
rng g3 = [#] (Closed-Interval-TSpace ((- 1),1)) )
by A1, Lm6, FUNCT_2:def 1;
(
g3 is
one-to-one & not
Upper_Arc P is
empty &
Upper_Arc P is
compact )
by A1, A13, Lm6, JORDAN5A:1;
then
g3 is
being_homeomorphism
by A23, A15, COMPTS_1:17;
then A24:
h is
being_homeomorphism
by A16, TOPMETR:20, TOPS_2:57;
A25:
dom g =
[#] I[01]
by A16, TOPS_2:def 5
.=
[.0,1.]
by BORSUK_1:40
;
then A26:
1
in dom g
by XXREAL_1:1;
A27: 1 =
|[1,0]| `1
by EUCLID:52
.=
g0 . |[1,0]|
by PSCOMP_1:def 5
.=
g3 . |[1,0]|
by A12, A14, FUNCT_1:49
.=
h . 1
by A12, A17, A26, FUNCT_1:13
;
A28:
s1 in [.0,1.]
by A19, XXREAL_1:1;
A29:
p2 `1 =
g0 . p2
by PSCOMP_1:def 5
.=
g3 . p2
by A9, FUNCT_1:49
.=
h . s2
by A20, A25, A22, FUNCT_1:13
;
p1 `1 =
g0 . p1
by PSCOMP_1:def 5
.=
g3 . p1
by A8, FUNCT_1:49
.=
h . s1
by A18, A25, A28, FUNCT_1:13
;
hence
s1 <= s2
by A6, A24, A28, A22, A27, A29, Th8;
verum
end;
then A30:
LE p1,p2, Upper_Arc P, W-min P, E-max P
by A8, A9, JORDAN5C:def 3;
p1 in Upper_Arc P
by A2, A4, A7;
hence
LE p1,p2,P
by A9, A30; verum