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 P4 = Lower_Arc P;
A10:
P is being_simple_closed_curve
by A1, JGRAPH_3:26;
then A11:
(Upper_Arc P) \/ (Lower_Arc P) = 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;
A15:
ex p3 being Point of (TOP-REAL 2) st
( p3 = p1 & |.p3.| = 1 )
by A1, A2;
A21:
(Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)}
by A10, JORDAN6:def 9;
A22:
Lower_Arc P is_an_arc_of E-max P, W-min P
by A10, JORDAN6:def 9;
A23:
W-min P = |[(- 1),0]|
by A1, Th29;
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
W-min P in {(W-min P),(E-max P)}
by TARSKI:def 2;
then A24:
W-min P in Lower_Arc P
by A21, XBOOLE_0:def 4;
set K0 =
Lower_Arc P;
reconsider g0 =
proj1 as
Function of
(TOP-REAL 2),
R^1 by TOPMETR:17;
reconsider g2 =
g0 | (Lower_Arc P) as
Function of
((TOP-REAL 2) | (Lower_Arc P)),
R^1 by PRE_TOPC:9;
Closed-Interval-TSpace (
(- 1),1)
= TopSpaceMetr (Closed-Interval-MSpace ((- 1),1))
by TOPMETR:def 7;
then A25:
Closed-Interval-TSpace (
(- 1),1) is
T_2
by PCOMPS_1:34;
reconsider g3 =
g2 as
continuous Function of
((TOP-REAL 2) | (Lower_Arc P)),
(Closed-Interval-TSpace ((- 1),1)) by A1, Lm5;
let g be
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 <= s2let s1,
s2 be
Real;
( 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 that A26:
g is
being_homeomorphism
and
g . 0 = E-max P
and A27:
g . 1
= W-min P
and A28:
g . s1 = p1
and A29:
(
0 <= s1 &
s1 <= 1 )
and A30:
g . s2 = p2
and A31:
(
0 <= s2 &
s2 <= 1 )
;
s1 <= s2
A32:
s2 in [.0,1.]
by A31, XXREAL_1:1;
reconsider h =
g3 * g as
Function of
(Closed-Interval-TSpace (0,1)),
(Closed-Interval-TSpace ((- 1),1)) by TOPMETR:20;
A33:
(
dom g3 = [#] ((TOP-REAL 2) | (Lower_Arc P)) &
rng g3 = [#] (Closed-Interval-TSpace ((- 1),1)) )
by A1, Lm5, FUNCT_2:def 1;
(
g3 is
one-to-one & not
Lower_Arc P is
empty &
Lower_Arc P is
compact )
by A1, A22, Lm5, JORDAN5A:1;
then
g3 is
being_homeomorphism
by A33, A25, COMPTS_1:17;
then A34:
h is
being_homeomorphism
by A26, TOPMETR:20, TOPS_2:57;
A35:
dom g =
[#] I[01]
by A26, TOPS_2:def 5
.=
[.0,1.]
by BORSUK_1:40
;
then A36:
1
in dom g
by XXREAL_1:1;
A37:
- 1 =
|[(- 1),0]| `1
by EUCLID:52
.=
proj1 . |[(- 1),0]|
by PSCOMP_1:def 5
.=
g3 . (g . 1)
by A23, A27, A24, FUNCT_1:49
.=
h . 1
by A36, FUNCT_1:13
;
A38:
s1 in [.0,1.]
by A29, XXREAL_1:1;
A39:
p2 `1 =
proj1 . p2
by PSCOMP_1:def 5
.=
g3 . (g . s2)
by A14, A30, FUNCT_1:49
.=
h . s2
by A35, A32, FUNCT_1:13
;
p1 `1 =
g0 . p1
by PSCOMP_1:def 5
.=
g3 . (g . s1)
by A13, A28, FUNCT_1:49
.=
h . s1
by A35, A38, FUNCT_1:13
;
hence
s1 <= s2
by A8, A16, A34, A38, A32, A37, A39, Th9;
verum
end;
then A40:
LE p1,p2, Lower_Arc P, E-max P, W-min P
by A13, A14, JORDAN5C:def 3;
hence
LE p1,p2,P
by A13, A14, A40; verum