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 `1 < 0 & p2 `1 < 0 & p1 `2 >= 0 & p2 `2 >= 0 & ( p1 `1 <= p2 `1 or p1 `2 <= p2 `2 ) 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 `1 < 0 & p2 `1 < 0 & p1 `2 >= 0 & p2 `2 >= 0 & ( p1 `1 <= p2 `1 or p1 `2 <= p2 `2 ) 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 `1 < 0
and
A5:
p2 `1 < 0
and
A6:
p1 `2 >= 0
and
A7:
p2 `2 >= 0
and
A8:
( p1 `1 <= p2 `1 or p1 `2 <= p2 `2 )
; LE p1,p2,P
A9:
ex p3 being Point of (TOP-REAL 2) st
( p3 = p2 & |.p3.| = 1 )
by A1, A3;
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:
Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
by A1, Th34;
then A13:
p1 in Upper_Arc P
by A2, A6;
A14:
p2 in Upper_Arc P
by A3, A7, A12;
A15:
ex p3 being Point of (TOP-REAL 2) st
( p3 = p1 & |.p3.| = 1 )
by A1, A2;
A21:
E-max P = |[1,0]|
by A1, Th30;
A22:
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 A23:
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 A24:
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 A25:
g is
being_homeomorphism
and
g . 0 = W-min P
and A26:
g . 1
= E-max P
and A27:
g . s1 = p1
and A28:
(
0 <= s1 &
s1 <= 1 )
and A29:
g . s2 = p2
and A30:
(
0 <= s2 &
s2 <= 1 )
;
s1 <= s2
A31:
s2 in [.0,1.]
by A30, XXREAL_1:1;
reconsider h =
g3 * g as
Function of
(Closed-Interval-TSpace (0,1)),
(Closed-Interval-TSpace ((- 1),1)) by TOPMETR:20;
A32:
(
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, A22, Lm6, JORDAN5A:1;
then
g3 is
being_homeomorphism
by A32, A24, COMPTS_1:17;
then A33:
h is
being_homeomorphism
by A25, TOPMETR:20, TOPS_2:57;
A34:
dom g =
[#] I[01]
by A25, TOPS_2:def 5
.=
[.0,1.]
by BORSUK_1:40
;
then A35:
1
in dom g
by XXREAL_1:1;
A36: 1 =
|[1,0]| `1
by EUCLID:52
.=
g0 . |[1,0]|
by PSCOMP_1:def 5
.=
g3 . |[1,0]|
by A21, A23, FUNCT_1:49
.=
h . 1
by A21, A26, A35, FUNCT_1:13
;
A37:
s1 in [.0,1.]
by A28, XXREAL_1:1;
A38:
p2 `1 =
g0 . p2
by PSCOMP_1:def 5
.=
g3 . p2
by A14, FUNCT_1:49
.=
h . s2
by A29, A34, A31, FUNCT_1:13
;
p1 `1 =
g0 . p1
by PSCOMP_1:def 5
.=
g3 . (g . s1)
by A13, A27, FUNCT_1:49
.=
h . s1
by A34, A37, FUNCT_1:13
;
hence
s1 <= s2
by A8, A16, A33, A37, A31, A36, A38, Th8;
verum
end;
then A39:
LE p1,p2, Upper_Arc P, W-min P, E-max P
by A13, A14, JORDAN5C:def 3;
p1 in Upper_Arc P
by A2, A6, A12;
hence
LE p1,p2,P
by A14, A39; verum