let a, b, c, d be Real; for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[a,c]|,|[b,c]|) & p2 in LSeg (|[a,c]|,|[b,c]|) holds
( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) )
let p1, p2 be Point of (TOP-REAL 2); ( a < b & c < d & p1 in LSeg (|[a,c]|,|[b,c]|) & p2 in LSeg (|[a,c]|,|[b,c]|) implies ( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) ) )
set K = rectangle (a,b,c,d);
assume that
A1:
a < b
and
A2:
c < d
and
A3:
p1 in LSeg (|[a,c]|,|[b,c]|)
and
A4:
p2 in LSeg (|[a,c]|,|[b,c]|)
; ( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) )
A5:
rectangle (a,b,c,d) is being_simple_closed_curve
by A1, A2, Th50;
A6:
p1 `2 = c
by A1, A3, Th3;
A7:
p1 `1 <= b
by A1, A3, Th3;
A8:
p2 `2 = c
by A1, A4, Th3;
A9:
a <= p2 `1
by A1, A4, Th3;
A10:
W-min (rectangle (a,b,c,d)) = |[a,c]|
by A1, A2, Th46;
A11:
E-max (rectangle (a,b,c,d)) = |[b,d]|
by A1, A2, Th46;
A12:
Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[b,d]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[a,c]|))
by A1, A2, Th52;
then A13:
LSeg (|[b,c]|,|[a,c]|) c= Lower_Arc (rectangle (a,b,c,d))
by XBOOLE_1:7;
then A14:
p1 in Lower_Arc (rectangle (a,b,c,d))
by A3;
A15:
Lower_Arc (rectangle (a,b,c,d)) c= rectangle (a,b,c,d)
by A5, JORDAN6:61;
A16:
(Upper_Arc (rectangle (a,b,c,d))) /\ (Lower_Arc (rectangle (a,b,c,d))) = {(W-min (rectangle (a,b,c,d))),(E-max (rectangle (a,b,c,d)))}
by A5, JORDAN6:def 9;
A17:
now ( p1 in Upper_Arc (rectangle (a,b,c,d)) implies p1 = W-min (rectangle (a,b,c,d)) )assume
p1 in Upper_Arc (rectangle (a,b,c,d))
;
p1 = W-min (rectangle (a,b,c,d))then
p1 in (Upper_Arc (rectangle (a,b,c,d))) /\ (Lower_Arc (rectangle (a,b,c,d)))
by A3, A13, XBOOLE_0:def 4;
then
(
p1 = W-min (rectangle (a,b,c,d)) or
p1 = E-max (rectangle (a,b,c,d)) )
by A16, TARSKI:def 2;
hence
p1 = W-min (rectangle (a,b,c,d))
by A2, A6, A11, EUCLID:52;
verum end;
thus
( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) implies ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) )
( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) implies ( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) ) )proof
assume that A18:
LE p1,
p2,
rectangle (
a,
b,
c,
d)
and A19:
p1 <> W-min (rectangle (a,b,c,d))
;
( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) )
A20:
( (
p1 in Upper_Arc (rectangle (a,b,c,d)) &
p2 in Lower_Arc (rectangle (a,b,c,d)) & not
p2 = W-min (rectangle (a,b,c,d)) ) or (
p1 in Upper_Arc (rectangle (a,b,c,d)) &
p2 in Upper_Arc (rectangle (a,b,c,d)) &
LE p1,
p2,
Upper_Arc (rectangle (a,b,c,d)),
W-min (rectangle (a,b,c,d)),
E-max (rectangle (a,b,c,d)) ) or (
p1 in Lower_Arc (rectangle (a,b,c,d)) &
p2 in Lower_Arc (rectangle (a,b,c,d)) & not
p2 = W-min (rectangle (a,b,c,d)) &
LE p1,
p2,
Lower_Arc (rectangle (a,b,c,d)),
E-max (rectangle (a,b,c,d)),
W-min (rectangle (a,b,c,d)) ) )
by A18, JORDAN6:def 10;
consider f being
Function of
I[01],
((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))) such that A21:
f is
being_homeomorphism
and A22:
f . 0 = E-max (rectangle (a,b,c,d))
and A23:
f . 1
= W-min (rectangle (a,b,c,d))
and
rng f = Lower_Arc (rectangle (a,b,c,d))
and
for
r being
Real st
r in [.0,(1 / 2).] holds
f . r = ((1 - (2 * r)) * |[b,d]|) + ((2 * r) * |[b,c]|)
and
for
r being
Real st
r in [.(1 / 2),1.] holds
f . r = ((1 - ((2 * r) - 1)) * |[b,c]|) + (((2 * r) - 1) * |[a,c]|)
and
for
p being
Point of
(TOP-REAL 2) st
p in LSeg (
|[b,d]|,
|[b,c]|) holds
(
0 <= (((p `2) - d) / (c - d)) / 2 &
(((p `2) - d) / (c - d)) / 2
<= 1 &
f . ((((p `2) - d) / (c - d)) / 2) = p )
and A24:
for
p being
Point of
(TOP-REAL 2) st
p in LSeg (
|[b,c]|,
|[a,c]|) holds
(
0 <= ((((p `1) - b) / (a - b)) / 2) + (1 / 2) &
((((p `1) - b) / (a - b)) / 2) + (1 / 2) <= 1 &
f . (((((p `1) - b) / (a - b)) / 2) + (1 / 2)) = p )
by A1, A2, Th54;
reconsider s1 =
((((p1 `1) - b) / (a - b)) / 2) + (1 / 2),
s2 =
((((p2 `1) - b) / (a - b)) / 2) + (1 / 2) as
Real ;
A25:
f . s1 = p1
by A3, A24;
A26:
f . s2 = p2
by A4, A24;
b - a > 0
by A1, XREAL_1:50;
then A27:
- (b - a) < - 0
by XREAL_1:24;
A28:
s1 <= 1
by A3, A24;
A29:
0 <= s2
by A4, A24;
s2 <= 1
by A4, A24;
then
s1 <= s2
by A17, A19, A20, A21, A22, A23, A25, A26, A28, A29, JORDAN5C:def 3;
then
(((p1 `1) - b) / (a - b)) / 2
<= (((p2 `1) - b) / (a - b)) / 2
by XREAL_1:6;
then
((((p1 `1) - b) / (a - b)) / 2) * 2
<= ((((p2 `1) - b) / (a - b)) / 2) * 2
by XREAL_1:64;
then
(((p1 `1) - b) / (a - b)) * (a - b) >= (((p2 `1) - b) / (a - b)) * (a - b)
by A27, XREAL_1:65;
then
(p1 `1) - b >= (((p2 `1) - b) / (a - b)) * (a - b)
by A27, XCMPLX_1:87;
then
(p1 `1) - b >= (p2 `1) - b
by A27, XCMPLX_1:87;
then
((p1 `1) - b) + b >= ((p2 `1) - b) + b
by XREAL_1:7;
hence
p1 `1 >= p2 `1
;
p2 <> W-min (rectangle (a,b,c,d))
now not p2 = W-min (rectangle (a,b,c,d))assume A30:
p2 = W-min (rectangle (a,b,c,d))
;
contradictionthen
LE p2,
p1,
rectangle (
a,
b,
c,
d)
by A5, A14, A15, JORDAN7:3;
hence
contradiction
by A1, A2, A18, A19, A30, Th50, JORDAN6:57;
verum end;
hence
p2 <> W-min (rectangle (a,b,c,d))
;
verum
end;
thus
( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) implies ( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) ) )
verumproof
assume that A31:
p1 `1 >= p2 `1
and A32:
p2 <> W-min (rectangle (a,b,c,d))
;
( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) )
A33:
for
g being
Function of
I[01],
((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))) for
s1,
s2 being
Real st
g is
being_homeomorphism &
g . 0 = E-max (rectangle (a,b,c,d)) &
g . 1
= W-min (rectangle (a,b,c,d)) &
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) | (Lower_Arc (rectangle (a,b,c,d))));
for s1, s2 being Real st g is being_homeomorphism & g . 0 = E-max (rectangle (a,b,c,d)) & g . 1 = W-min (rectangle (a,b,c,d)) & 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 (rectangle (a,b,c,d)) & g . 1 = W-min (rectangle (a,b,c,d)) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume that A34:
g is
being_homeomorphism
and A35:
g . 0 = E-max (rectangle (a,b,c,d))
and
g . 1
= W-min (rectangle (a,b,c,d))
and A36:
g . s1 = p1
and A37:
0 <= s1
and A38:
s1 <= 1
and A39:
g . s2 = p2
and A40:
0 <= s2
and A41:
s2 <= 1
;
s1 <= s2
A42:
dom g = the
carrier of
I[01]
by FUNCT_2:def 1;
A43:
g is
one-to-one
by A34, TOPS_2:def 5;
A44:
the
carrier of
((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))) = Lower_Arc (rectangle (a,b,c,d))
by PRE_TOPC:8;
then reconsider g1 =
g as
Function of
I[01],
(TOP-REAL 2) by FUNCT_2:7;
g is
continuous
by A34, TOPS_2:def 5;
then A45:
g1 is
continuous
by PRE_TOPC:26;
reconsider h1 =
proj1 as
Function of
(TOP-REAL 2),
R^1 by TOPMETR:17;
reconsider h2 =
proj2 as
Function of
(TOP-REAL 2),
R^1 by TOPMETR:17;
reconsider hh1 =
h1 as
Function of
TopStruct(# the
carrier of
(TOP-REAL 2), the
topology of
(TOP-REAL 2) #),
R^1 ;
reconsider hh2 =
h2 as
Function of
TopStruct(# the
carrier of
(TOP-REAL 2), the
topology of
(TOP-REAL 2) #),
R^1 ;
A46:
TopStruct(# the
carrier of
(TOP-REAL 2), the
topology of
(TOP-REAL 2) #) =
TopStruct(# the
carrier of
(TOP-REAL 2), the
topology of
(TOP-REAL 2) #)
| ([#] TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #))
by TSEP_1:3
.=
TopStruct(# the
carrier of
((TOP-REAL 2) | ([#] (TOP-REAL 2))), the
topology of
((TOP-REAL 2) | ([#] (TOP-REAL 2))) #)
by PRE_TOPC:36
.=
(TOP-REAL 2) | ([#] (TOP-REAL 2))
;
then
( ( for
p being
Point of
((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds
hh1 . p = proj1 . p ) implies
hh1 is
continuous )
by JGRAPH_2:29;
then A47:
( ( for
p being
Point of
((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds
hh1 . p = proj1 . p ) implies
h1 is
continuous )
by PRE_TOPC:32;
( ( for
p being
Point of
((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds
hh2 . p = proj2 . p ) implies
hh2 is
continuous )
by A46, JGRAPH_2:30;
then
( ( for
p being
Point of
((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds
hh2 . p = proj2 . p ) implies
h2 is
continuous )
by PRE_TOPC:32;
then consider h being
Function of
(TOP-REAL 2),
R^1 such that A48:
for
p being
Point of
(TOP-REAL 2) for
r1,
r2 being
Real st
h1 . p = r1 &
h2 . p = r2 holds
h . p = r1 + r2
and A49:
h is
continuous
by A47, JGRAPH_2:19;
reconsider k =
h * g1 as
Function of
I[01],
R^1 ;
A50:
E-max (rectangle (a,b,c,d)) = |[b,d]|
by A1, A2, Th46;
now not s1 > s2assume A51:
s1 > s2
;
contradictionA52:
dom g = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
0 in [.0,1.]
by XXREAL_1:1;
then A53:
k . 0 =
h . (E-max (rectangle (a,b,c,d)))
by A35, A52, FUNCT_1:13
.=
(h1 . (E-max (rectangle (a,b,c,d)))) + (h2 . (E-max (rectangle (a,b,c,d))))
by A48
.=
((E-max (rectangle (a,b,c,d))) `1) + (proj2 . (E-max (rectangle (a,b,c,d))))
by PSCOMP_1:def 5
.=
((E-max (rectangle (a,b,c,d))) `1) + ((E-max (rectangle (a,b,c,d))) `2)
by PSCOMP_1:def 6
.=
((E-max (rectangle (a,b,c,d))) `1) + d
by A50, EUCLID:52
.=
b + d
by A50, EUCLID:52
;
s1 in [.0,1.]
by A37, A38, XXREAL_1:1;
then A54:
k . s1 =
h . p1
by A36, A52, FUNCT_1:13
.=
(proj1 . p1) + (proj2 . p1)
by A48
.=
(p1 `1) + (proj2 . p1)
by PSCOMP_1:def 5
.=
(p1 `1) + c
by A6, PSCOMP_1:def 6
;
A55:
s2 in [.0,1.]
by A40, A41, XXREAL_1:1;
then A56:
k . s2 =
h . p2
by A39, A52, FUNCT_1:13
.=
(h1 . p2) + (h2 . p2)
by A48
.=
(p2 `1) + (proj2 . p2)
by PSCOMP_1:def 5
.=
(p2 `1) + c
by A8, PSCOMP_1:def 6
;
A57:
k . 0 >= k . s1
by A2, A7, A53, A54, XREAL_1:7;
A58:
k . s1 >= k . s2
by A31, A54, A56, XREAL_1:7;
A59:
0 in [.0,1.]
by XXREAL_1:1;
then A60:
[.0,s2.] c= [.0,1.]
by A55, XXREAL_2:def 12;
reconsider B =
[.0,s2.] as
Subset of
I[01] by A55, A59, BORSUK_1:40, XXREAL_2:def 12;
A61:
B is
connected
by A40, A55, A59, BORSUK_1:40, BORSUK_4:24;
A62:
0 in B
by A40, XXREAL_1:1;
A63:
s2 in B
by A40, XXREAL_1:1;
consider xc being
Point of
I[01] such that A64:
xc in B
and A65:
k . xc = k . s1
by A45, A49, A57, A58, A61, A62, A63, TOPREAL5:5;
reconsider rxc =
xc as
Real ;
A66:
for
x1,
x2 being
set st
x1 in dom k &
x2 in dom k &
k . x1 = k . x2 holds
x1 = x2
proof
let x1,
x2 be
set ;
( x1 in dom k & x2 in dom k & k . x1 = k . x2 implies x1 = x2 )
assume that A67:
x1 in dom k
and A68:
x2 in dom k
and A69:
k . x1 = k . x2
;
x1 = x2
reconsider r1 =
x1 as
Point of
I[01] by A67;
reconsider r2 =
x2 as
Point of
I[01] by A68;
A70:
k . x1 =
h . (g1 . x1)
by A67, FUNCT_1:12
.=
(h1 . (g1 . r1)) + (h2 . (g1 . r1))
by A48
.=
((g1 . r1) `1) + (proj2 . (g1 . r1))
by PSCOMP_1:def 5
.=
((g1 . r1) `1) + ((g1 . r1) `2)
by PSCOMP_1:def 6
;
A71:
k . x2 =
h . (g1 . x2)
by A68, FUNCT_1:12
.=
(h1 . (g1 . r2)) + (h2 . (g1 . r2))
by A48
.=
((g1 . r2) `1) + (proj2 . (g1 . r2))
by PSCOMP_1:def 5
.=
((g1 . r2) `1) + ((g1 . r2) `2)
by PSCOMP_1:def 6
;
A72:
g . r1 in Lower_Arc (rectangle (a,b,c,d))
by A44;
A73:
g . r2 in Lower_Arc (rectangle (a,b,c,d))
by A44;
reconsider gr1 =
g . r1 as
Point of
(TOP-REAL 2) by A72;
reconsider gr2 =
g . r2 as
Point of
(TOP-REAL 2) by A73;
now ( ( g . r1 in LSeg (|[b,d]|,|[b,c]|) & g . r2 in LSeg (|[b,d]|,|[b,c]|) & x1 = x2 ) or ( g . r1 in LSeg (|[b,d]|,|[b,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) & x1 = x2 ) or ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,d]|,|[b,c]|) & x1 = x2 ) or ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) & x1 = x2 ) )per cases
( ( g . r1 in LSeg (|[b,d]|,|[b,c]|) & g . r2 in LSeg (|[b,d]|,|[b,c]|) ) or ( g . r1 in LSeg (|[b,d]|,|[b,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) ) or ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,d]|,|[b,c]|) ) or ( g . r1 in LSeg (|[b,c]|,|[a,c]|) & g . r2 in LSeg (|[b,c]|,|[a,c]|) ) )
by A12, A44, XBOOLE_0:def 3;
case A74:
(
g . r1 in LSeg (
|[b,d]|,
|[b,c]|) &
g . r2 in LSeg (
|[b,d]|,
|[b,c]|) )
;
x1 = x2then A75:
gr1 `1 = b
by A2, Th1;
gr2 `1 = b
by A2, A74, Th1;
then
|[(gr1 `1),(gr1 `2)]| = g . r2
by A69, A70, A71, A75, EUCLID:53;
then
g . r1 = g . r2
by EUCLID:53;
hence
x1 = x2
by A42, A43, FUNCT_1:def 4;
verum end; case A76:
(
g . r1 in LSeg (
|[b,d]|,
|[b,c]|) &
g . r2 in LSeg (
|[b,c]|,
|[a,c]|) )
;
x1 = x2then A77:
gr1 `1 = b
by A2, Th1;
A78:
c <= gr1 `2
by A2, A76, Th1;
A79:
gr2 `2 = c
by A1, A76, Th3;
A80:
gr2 `1 <= b
by A1, A76, Th3;
A81:
b + (gr1 `2) = (gr2 `1) + c
by A1, A69, A70, A71, A76, A77, Th3;
then
|[(gr1 `1),(gr1 `2)]| = g . r2
by A77, A79, A82, EUCLID:53;
then
g . r1 = g . r2
by EUCLID:53;
hence
x1 = x2
by A42, A43, FUNCT_1:def 4;
verum end; case A83:
(
g . r1 in LSeg (
|[b,c]|,
|[a,c]|) &
g . r2 in LSeg (
|[b,d]|,
|[b,c]|) )
;
x1 = x2then A84:
gr2 `1 = b
by A2, Th1;
A85:
c <= gr2 `2
by A2, A83, Th1;
A86:
gr1 `2 = c
by A1, A83, Th3;
A87:
gr1 `1 <= b
by A1, A83, Th3;
A88:
b + (gr2 `2) = (gr1 `1) + c
by A1, A69, A70, A71, A83, A84, Th3;
then
|[(gr2 `1),(gr2 `2)]| = g . r1
by A84, A86, A89, EUCLID:53;
then
g . r1 = g . r2
by EUCLID:53;
hence
x1 = x2
by A42, A43, FUNCT_1:def 4;
verum end; case A90:
(
g . r1 in LSeg (
|[b,c]|,
|[a,c]|) &
g . r2 in LSeg (
|[b,c]|,
|[a,c]|) )
;
x1 = x2then A91:
gr1 `2 = c
by A1, Th3;
gr2 `2 = c
by A1, A90, Th3;
then
|[(gr1 `1),(gr1 `2)]| = g . r2
by A69, A70, A71, A91, EUCLID:53;
then
g . r1 = g . r2
by EUCLID:53;
hence
x1 = x2
by A42, A43, FUNCT_1:def 4;
verum end;
hence
x1 = x2
;
verum
end; A92:
dom k = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
then
s1 in dom k
by A37, A38, XXREAL_1:1;
then
rxc = s1
by A60, A64, A65, A66, A92;
hence
contradiction
by A51, A64, XXREAL_1:1;
verum end;
hence
s1 <= s2
;
verum
end;
A93:
now not p1 = W-min (rectangle (a,b,c,d))assume A94:
p1 = W-min (rectangle (a,b,c,d))
;
contradictionthen
p1 `1 = a
by A10, EUCLID:52;
then
p1 `1 = p2 `1
by A9, A31, XXREAL_0:1;
then
|[(p1 `1),(p1 `2)]| = p2
by A6, A8, EUCLID:53;
hence
contradiction
by A32, A94, EUCLID:53;
verum end;
LE p1,
p2,
Lower_Arc (rectangle (a,b,c,d)),
E-max (rectangle (a,b,c,d)),
W-min (rectangle (a,b,c,d))
by A3, A4, A13, A33, JORDAN5C:def 3;
hence
LE p1,
p2,
rectangle (
a,
b,
c,
d)
by A3, A4, A13, A32, JORDAN6:def 10;
p1 <> W-min (rectangle (a,b,c,d))
thus
p1 <> W-min (rectangle (a,b,c,d))
by A93;
verum
end;