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 & p2 <> W-min P & 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 & p2 <> W-min P & 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:
p2 <> W-min P
and
A7:
p1 `1 >= p2 `1
; LE p1,p2,P
A8:
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) }
by A1, Th35;
then A9:
p1 in Lower_Arc P
by A2, A4;
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:
W-min P = |[(- 1),0]|
by A1, Th29;
A13:
p2 in Lower_Arc P
by A3, A5, A8;
A14:
Lower_Arc P is_an_arc_of E-max P, W-min P
by A10, JORDAN6:def 9;
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 A15:
W-min P in Lower_Arc P
by A11, 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 A16:
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 A17:
g is
being_homeomorphism
and
g . 0 = E-max P
and A18:
g . 1
= W-min P
and A19:
g . s1 = p1
and A20:
(
0 <= s1 &
s1 <= 1 )
and A21:
g . s2 = p2
and A22:
(
0 <= s2 &
s2 <= 1 )
;
s1 <= s2
A23:
s2 in [.0,1.]
by A22, XXREAL_1:1;
reconsider h =
g3 * g as
Function of
(Closed-Interval-TSpace (0,1)),
(Closed-Interval-TSpace ((- 1),1)) by TOPMETR:20;
A24:
(
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, A14, Lm5, JORDAN5A:1;
then
g3 is
being_homeomorphism
by A24, A16, COMPTS_1:17;
then A25:
h is
being_homeomorphism
by A17, TOPMETR:20, TOPS_2:57;
A26:
dom g =
[#] I[01]
by A17, TOPS_2:def 5
.=
[.0,1.]
by BORSUK_1:40
;
then A27:
1
in dom g
by XXREAL_1:1;
A28:
- 1 =
|[(- 1),0]| `1
by EUCLID:52
.=
proj1 . |[(- 1),0]|
by PSCOMP_1:def 5
.=
g3 . |[(- 1),0]|
by A12, A15, FUNCT_1:49
.=
h . 1
by A12, A18, A27, FUNCT_1:13
;
A29:
s1 in [.0,1.]
by A20, XXREAL_1:1;
A30:
p2 `1 =
g0 . p2
by PSCOMP_1:def 5
.=
g3 . p2
by A13, FUNCT_1:49
.=
h . s2
by A21, A26, A23, FUNCT_1:13
;
p1 `1 =
g0 . p1
by PSCOMP_1:def 5
.=
g3 . p1
by A9, FUNCT_1:49
.=
h . s1
by A19, A26, A29, FUNCT_1:13
;
hence
s1 <= s2
by A7, A25, A29, A23, A28, A30, Th9;
verum
end;
then A31:
LE p1,p2, Lower_Arc P, E-max P, W-min P
by A9, A13, JORDAN5C:def 3;
( p1 in Lower_Arc P & p2 in Lower_Arc P )
by A2, A3, A4, A5, A8;
hence
LE p1,p2,P
by A6, A31; verum