let a, b, c, d be Real; for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[b,d]|,|[b,c]|) holds
( LE p1,p2, rectangle (a,b,c,d) iff ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) )
let p1, p2 be Point of (TOP-REAL 2); ( a < b & c < d & p1 in LSeg (|[b,d]|,|[b,c]|) implies ( LE p1,p2, rectangle (a,b,c,d) iff ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & 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 (|[b,d]|,|[b,c]|)
; ( LE p1,p2, rectangle (a,b,c,d) iff ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) )
A4:
rectangle (a,b,c,d) is being_simple_closed_curve
by A1, A2, Th50;
A5:
p1 `1 = b
by A2, A3, Th1;
A6:
c <= p1 `2
by A2, A3, Th1;
A7:
p1 `2 <= d
by A2, A3, Th1;
thus
( not LE p1,p2, rectangle (a,b,c,d) or ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )
( ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) implies LE p1,p2, rectangle (a,b,c,d) )proof
assume A8:
LE p1,
p2,
rectangle (
a,
b,
c,
d)
;
( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )
then A9:
p1 in rectangle (
a,
b,
c,
d)
by A4, JORDAN7:5;
A10:
p2 in rectangle (
a,
b,
c,
d)
by A4, A8, JORDAN7:5;
rectangle (
a,
b,
c,
d) =
((LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|))) \/ ((LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|)))
by SPPOL_2:def 3
.=
(((LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|))) \/ (LSeg (|[b,d]|,|[b,c]|))) \/ (LSeg (|[b,c]|,|[a,c]|))
by XBOOLE_1:4
;
then
(
p2 in ((LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|))) \/ (LSeg (|[b,d]|,|[b,c]|)) or
p2 in LSeg (
|[b,c]|,
|[a,c]|) )
by A10, XBOOLE_0:def 3;
then A11:
(
p2 in (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) or
p2 in LSeg (
|[b,d]|,
|[b,c]|) or
p2 in LSeg (
|[b,c]|,
|[a,c]|) )
by XBOOLE_0:def 3;
now ( ( p2 in LSeg (|[a,c]|,|[a,d]|) & ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ) or ( p2 in LSeg (|[a,d]|,|[b,d]|) & ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ) or ( p2 in LSeg (|[b,d]|,|[b,c]|) & ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ) )per cases
( p2 in LSeg (|[a,c]|,|[a,d]|) or p2 in LSeg (|[a,d]|,|[b,d]|) or p2 in LSeg (|[b,d]|,|[b,c]|) or p2 in LSeg (|[b,c]|,|[a,c]|) )
by A11, XBOOLE_0:def 3;
case
p2 in LSeg (
|[a,c]|,
|[a,d]|)
;
( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )then
LE p2,
p1,
rectangle (
a,
b,
c,
d)
by A1, A2, A3, Th59;
hence
( (
p2 in LSeg (
|[b,d]|,
|[b,c]|) &
p1 `2 >= p2 `2 ) or (
p2 in LSeg (
|[b,c]|,
|[a,c]|) &
p2 <> W-min (rectangle (a,b,c,d)) ) )
by A1, A2, A3, A8, Th50, JORDAN6:57;
verum end; case
p2 in LSeg (
|[a,d]|,
|[b,d]|)
;
( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )then
LE p2,
p1,
rectangle (
a,
b,
c,
d)
by A1, A2, A3, Th60;
hence
( (
p2 in LSeg (
|[b,d]|,
|[b,c]|) &
p1 `2 >= p2 `2 ) or (
p2 in LSeg (
|[b,c]|,
|[a,c]|) &
p2 <> W-min (rectangle (a,b,c,d)) ) )
by A1, A2, A3, A8, Th50, JORDAN6:57;
verum end; case
p2 in LSeg (
|[b,d]|,
|[b,c]|)
;
( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )hence
( (
p2 in LSeg (
|[b,d]|,
|[b,c]|) &
p1 `2 >= p2 `2 ) or (
p2 in LSeg (
|[b,c]|,
|[a,c]|) &
p2 <> W-min (rectangle (a,b,c,d)) ) )
by A1, A2, A3, A8, Th57;
verum end; case A12:
p2 in LSeg (
|[b,c]|,
|[a,c]|)
;
( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )now ( ( p2 = W-min (rectangle (a,b,c,d)) & ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ) or ( p2 <> W-min (rectangle (a,b,c,d)) & ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ) )per cases
( p2 = W-min (rectangle (a,b,c,d)) or p2 <> W-min (rectangle (a,b,c,d)) )
;
case
p2 = W-min (rectangle (a,b,c,d))
;
( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )then
LE p2,
p1,
rectangle (
a,
b,
c,
d)
by A4, A9, JORDAN7:3;
hence
( (
p2 in LSeg (
|[b,d]|,
|[b,c]|) &
p1 `2 >= p2 `2 ) or (
p2 in LSeg (
|[b,c]|,
|[a,c]|) &
p2 <> W-min (rectangle (a,b,c,d)) ) )
by A1, A2, A3, A8, Th50, JORDAN6:57;
verum end; case
p2 <> W-min (rectangle (a,b,c,d))
;
( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )end; end; end; hence
( (
p2 in LSeg (
|[b,d]|,
|[b,c]|) &
p1 `2 >= p2 `2 ) or (
p2 in LSeg (
|[b,c]|,
|[a,c]|) &
p2 <> W-min (rectangle (a,b,c,d)) ) )
;
verum end; end; end;
hence
( (
p2 in LSeg (
|[b,d]|,
|[b,c]|) &
p1 `2 >= p2 `2 ) or (
p2 in LSeg (
|[b,c]|,
|[a,c]|) &
p2 <> W-min (rectangle (a,b,c,d)) ) )
;
verum
end;
thus
( ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) implies LE p1,p2, rectangle (a,b,c,d) )
verumproof
assume A13:
( (
p2 in LSeg (
|[b,d]|,
|[b,c]|) &
p1 `2 >= p2 `2 ) or (
p2 in LSeg (
|[b,c]|,
|[a,c]|) &
p2 <> W-min (rectangle (a,b,c,d)) ) )
;
LE p1,p2, rectangle (a,b,c,d)
now ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 & LE p1,p2, rectangle (a,b,c,d) ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) & LE p1,p2, rectangle (a,b,c,d) ) )per cases
( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) )
by A13;
case A14:
(
p2 in LSeg (
|[b,d]|,
|[b,c]|) &
p1 `2 >= p2 `2 )
;
LE p1,p2, rectangle (a,b,c,d)then A15:
p2 `1 = b
by A2, Th1;
W-min (rectangle (a,b,c,d)) = |[a,c]|
by A1, A2, Th46;
then A16:
p2 <> W-min (rectangle (a,b,c,d))
by A1, A15, EUCLID:52;
A17:
Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[b,d]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[a,c]|))
by A1, A2, Th52;
then A18:
p2 in Lower_Arc (rectangle (a,b,c,d))
by A14, XBOOLE_0:def 3;
A19:
p1 in Lower_Arc (rectangle (a,b,c,d))
by A3, A17, XBOOLE_0:def 3;
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 A20:
g is
being_homeomorphism
and A21:
g . 0 = E-max (rectangle (a,b,c,d))
and
g . 1
= W-min (rectangle (a,b,c,d))
and A22:
g . s1 = p1
and A23:
0 <= s1
and A24:
s1 <= 1
and A25:
g . s2 = p2
and A26:
0 <= s2
and A27:
s2 <= 1
;
s1 <= s2
A28:
dom g = the
carrier of
I[01]
by FUNCT_2:def 1;
A29:
g is
one-to-one
by A20, TOPS_2:def 5;
A30:
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 A20, TOPS_2:def 5;
then A31:
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 ;
A32:
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 A33:
( ( 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 A32, 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 A34:
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 A35:
h is
continuous
by A33, JGRAPH_2:19;
reconsider k =
h * g1 as
Function of
I[01],
R^1 ;
A36:
E-max (rectangle (a,b,c,d)) = |[b,d]|
by A1, A2, Th46;
now not s1 > s2assume A37:
s1 > s2
;
contradictionA38:
dom g = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
0 in [.0,1.]
by XXREAL_1:1;
then A39:
k . 0 =
h . (E-max (rectangle (a,b,c,d)))
by A21, A38, FUNCT_1:13
.=
(h1 . (E-max (rectangle (a,b,c,d)))) + (h2 . (E-max (rectangle (a,b,c,d))))
by A34
.=
((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 A36, EUCLID:52
.=
b + d
by A36, EUCLID:52
;
s1 in [.0,1.]
by A23, A24, XXREAL_1:1;
then A40:
k . s1 =
h . p1
by A22, A38, FUNCT_1:13
.=
(proj1 . p1) + (proj2 . p1)
by A34
.=
(p1 `1) + (proj2 . p1)
by PSCOMP_1:def 5
.=
b + (p1 `2)
by A5, PSCOMP_1:def 6
;
A41:
s2 in [.0,1.]
by A26, A27, XXREAL_1:1;
then A42:
k . s2 =
h . p2
by A25, A38, FUNCT_1:13
.=
(proj1 . p2) + (proj2 . p2)
by A34
.=
(p2 `1) + (proj2 . p2)
by PSCOMP_1:def 5
.=
b + (p2 `2)
by A15, PSCOMP_1:def 6
;
A43:
k . 0 >= k . s1
by A7, A39, A40, XREAL_1:7;
A44:
k . s1 >= k . s2
by A14, A40, A42, XREAL_1:7;
A45:
0 in [.0,1.]
by XXREAL_1:1;
then A46:
[.0,s2.] c= [.0,1.]
by A41, XXREAL_2:def 12;
reconsider B =
[.0,s2.] as
Subset of
I[01] by A41, A45, BORSUK_1:40, XXREAL_2:def 12;
A47:
B is
connected
by A26, A41, A45, BORSUK_1:40, BORSUK_4:24;
A48:
0 in B
by A26, XXREAL_1:1;
A49:
s2 in B
by A26, XXREAL_1:1;
consider xc being
Point of
I[01] such that A50:
xc in B
and A51:
k . xc = k . s1
by A31, A35, A43, A44, A47, A48, A49, TOPREAL5:5;
reconsider rxc =
xc as
Real ;
A52:
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 A53:
x1 in dom k
and A54:
x2 in dom k
and A55:
k . x1 = k . x2
;
x1 = x2
reconsider r1 =
x1 as
Point of
I[01] by A53;
reconsider r2 =
x2 as
Point of
I[01] by A54;
A56:
k . x1 =
h . (g1 . x1)
by A53, FUNCT_1:12
.=
(h1 . (g1 . r1)) + (h2 . (g1 . r1))
by A34
.=
((g1 . r1) `1) + (proj2 . (g1 . r1))
by PSCOMP_1:def 5
.=
((g1 . r1) `1) + ((g1 . r1) `2)
by PSCOMP_1:def 6
;
A57:
k . x2 =
h . (g1 . x2)
by A54, FUNCT_1:12
.=
(h1 . (g1 . r2)) + (h2 . (g1 . r2))
by A34
.=
((g1 . r2) `1) + (proj2 . (g1 . r2))
by PSCOMP_1:def 5
.=
((g1 . r2) `1) + ((g1 . r2) `2)
by PSCOMP_1:def 6
;
A58:
g . r1 in Lower_Arc (rectangle (a,b,c,d))
by A30;
A59:
g . r2 in Lower_Arc (rectangle (a,b,c,d))
by A30;
reconsider gr1 =
g . r1 as
Point of
(TOP-REAL 2) by A58;
reconsider gr2 =
g . r2 as
Point of
(TOP-REAL 2) by A59;
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 A17, A30, XBOOLE_0:def 3;
case A60:
(
g . r1 in LSeg (
|[b,d]|,
|[b,c]|) &
g . r2 in LSeg (
|[b,d]|,
|[b,c]|) )
;
x1 = x2then A61:
gr1 `1 = b
by A2, Th1;
gr2 `1 = b
by A2, A60, Th1;
then
|[(gr1 `1),(gr1 `2)]| = g . r2
by A55, A56, A57, A61, EUCLID:53;
then
g . r1 = g . r2
by EUCLID:53;
hence
x1 = x2
by A28, A29, FUNCT_1:def 4;
verum end; case A62:
(
g . r1 in LSeg (
|[b,d]|,
|[b,c]|) &
g . r2 in LSeg (
|[b,c]|,
|[a,c]|) )
;
x1 = x2then A63:
gr1 `1 = b
by A2, Th1;
A64:
c <= gr1 `2
by A2, A62, Th1;
A65:
gr2 `2 = c
by A1, A62, Th3;
A66:
gr2 `1 <= b
by A1, A62, Th3;
A67:
b + (gr1 `2) = (gr2 `1) + c
by A2, A55, A56, A57, A62, A65, Th1;
then
|[(gr1 `1),(gr1 `2)]| = g . r2
by A63, A65, A68, EUCLID:53;
then
g . r1 = g . r2
by EUCLID:53;
hence
x1 = x2
by A28, A29, FUNCT_1:def 4;
verum end; case A69:
(
g . r1 in LSeg (
|[b,c]|,
|[a,c]|) &
g . r2 in LSeg (
|[b,d]|,
|[b,c]|) )
;
x1 = x2then A70:
gr2 `1 = b
by A2, Th1;
A71:
c <= gr2 `2
by A2, A69, Th1;
A72:
gr1 `2 = c
by A1, A69, Th3;
A73:
gr1 `1 <= b
by A1, A69, Th3;
A74:
b + (gr2 `2) = (gr1 `1) + c
by A1, A55, A56, A57, A69, A70, Th3;
then
|[(gr2 `1),(gr2 `2)]| = g . r1
by A70, A72, A75, EUCLID:53;
then
g . r1 = g . r2
by EUCLID:53;
hence
x1 = x2
by A28, A29, FUNCT_1:def 4;
verum end; case A76:
(
g . r1 in LSeg (
|[b,c]|,
|[a,c]|) &
g . r2 in LSeg (
|[b,c]|,
|[a,c]|) )
;
x1 = x2then A77:
gr1 `2 = c
by A1, Th3;
gr2 `2 = c
by A1, A76, Th3;
then
|[(gr1 `1),(gr1 `2)]| = g . r2
by A55, A56, A57, A77, EUCLID:53;
then
g . r1 = g . r2
by EUCLID:53;
hence
x1 = x2
by A28, A29, FUNCT_1:def 4;
verum end; end; end;
hence
x1 = x2
;
verum
end; A78:
dom k = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
then
s1 in dom k
by A23, A24, XXREAL_1:1;
then
rxc = s1
by A46, A50, A51, A52, A78;
hence
contradiction
by A37, A50, XXREAL_1:1;
verum end;
hence
s1 <= s2
;
verum
end; then
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, A19, JORDAN5C:def 3;
hence
LE p1,
p2,
rectangle (
a,
b,
c,
d)
by A16, A18, A19, JORDAN6:def 10;
verum end; case A79:
(
p2 in LSeg (
|[b,c]|,
|[a,c]|) &
p2 <> W-min (rectangle (a,b,c,d)) )
;
LE p1,p2, rectangle (a,b,c,d)then A80:
p2 `2 = c
by A1, Th3;
A81:
p2 `1 <= b
by A1, A79, Th3;
A82:
Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[b,d]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[a,c]|))
by A1, A2, Th52;
then A83:
p2 in Lower_Arc (rectangle (a,b,c,d))
by A79, XBOOLE_0:def 3;
A84:
p1 in Lower_Arc (rectangle (a,b,c,d))
by A3, A82, XBOOLE_0:def 3;
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 A85:
g is
being_homeomorphism
and A86:
g . 0 = E-max (rectangle (a,b,c,d))
and
g . 1
= W-min (rectangle (a,b,c,d))
and A87:
g . s1 = p1
and A88:
0 <= s1
and A89:
s1 <= 1
and A90:
g . s2 = p2
and A91:
0 <= s2
and A92:
s2 <= 1
;
s1 <= s2
A93:
dom g = the
carrier of
I[01]
by FUNCT_2:def 1;
A94:
g is
one-to-one
by A85, TOPS_2:def 5;
A95:
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 A85, TOPS_2:def 5;
then A96:
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 ;
A97:
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 A98:
( ( 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 A97, 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 A99:
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 A100:
h is
continuous
by A98, JGRAPH_2:19;
reconsider k =
h * g1 as
Function of
I[01],
R^1 ;
A101:
E-max (rectangle (a,b,c,d)) = |[b,d]|
by A1, A2, Th46;
now not s1 > s2assume A102:
s1 > s2
;
contradictionA103:
dom g = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
0 in [.0,1.]
by XXREAL_1:1;
then A104:
k . 0 =
h . (E-max (rectangle (a,b,c,d)))
by A86, A103, FUNCT_1:13
.=
(h1 . (E-max (rectangle (a,b,c,d)))) + (h2 . (E-max (rectangle (a,b,c,d))))
by A99
.=
((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 A101, EUCLID:52
.=
b + d
by A101, EUCLID:52
;
s1 in [.0,1.]
by A88, A89, XXREAL_1:1;
then A105:
k . s1 =
h . p1
by A87, A103, FUNCT_1:13
.=
(proj1 . p1) + (proj2 . p1)
by A99
.=
(p1 `1) + (proj2 . p1)
by PSCOMP_1:def 5
.=
b + (p1 `2)
by A5, PSCOMP_1:def 6
;
A106:
s2 in [.0,1.]
by A91, A92, XXREAL_1:1;
then A107:
k . s2 =
h . p2
by A90, A103, FUNCT_1:13
.=
(proj1 . p2) + (proj2 . p2)
by A99
.=
(p2 `1) + (proj2 . p2)
by PSCOMP_1:def 5
.=
(p2 `1) + c
by A80, PSCOMP_1:def 6
;
A108:
k . 0 >= k . s1
by A7, A104, A105, XREAL_1:7;
A109:
k . s1 >= k . s2
by A6, A81, A105, A107, XREAL_1:7;
A110:
0 in [.0,1.]
by XXREAL_1:1;
then A111:
[.0,s2.] c= [.0,1.]
by A106, XXREAL_2:def 12;
reconsider B =
[.0,s2.] as
Subset of
I[01] by A106, A110, BORSUK_1:40, XXREAL_2:def 12;
A112:
B is
connected
by A91, A106, A110, BORSUK_1:40, BORSUK_4:24;
A113:
0 in B
by A91, XXREAL_1:1;
A114:
s2 in B
by A91, XXREAL_1:1;
consider xc being
Point of
I[01] such that A115:
xc in B
and A116:
k . xc = k . s1
by A96, A100, A108, A109, A112, A113, A114, TOPREAL5:5;
reconsider rxc =
xc as
Real ;
A117:
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 A118:
x1 in dom k
and A119:
x2 in dom k
and A120:
k . x1 = k . x2
;
x1 = x2
reconsider r1 =
x1 as
Point of
I[01] by A118;
reconsider r2 =
x2 as
Point of
I[01] by A119;
A121:
k . x1 =
h . (g1 . x1)
by A118, FUNCT_1:12
.=
(h1 . (g1 . r1)) + (h2 . (g1 . r1))
by A99
.=
((g1 . r1) `1) + (proj2 . (g1 . r1))
by PSCOMP_1:def 5
.=
((g1 . r1) `1) + ((g1 . r1) `2)
by PSCOMP_1:def 6
;
A122:
k . x2 =
h . (g1 . x2)
by A119, FUNCT_1:12
.=
(h1 . (g1 . r2)) + (h2 . (g1 . r2))
by A99
.=
((g1 . r2) `1) + (proj2 . (g1 . r2))
by PSCOMP_1:def 5
.=
((g1 . r2) `1) + ((g1 . r2) `2)
by PSCOMP_1:def 6
;
A123:
g . r1 in Lower_Arc (rectangle (a,b,c,d))
by A95;
A124:
g . r2 in Lower_Arc (rectangle (a,b,c,d))
by A95;
reconsider gr1 =
g . r1 as
Point of
(TOP-REAL 2) by A123;
reconsider gr2 =
g . r2 as
Point of
(TOP-REAL 2) by A124;
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 A82, A95, XBOOLE_0:def 3;
case A125:
(
g . r1 in LSeg (
|[b,d]|,
|[b,c]|) &
g . r2 in LSeg (
|[b,d]|,
|[b,c]|) )
;
x1 = x2then A126:
gr1 `1 = b
by A2, Th1;
gr2 `1 = b
by A2, A125, Th1;
then
|[(gr1 `1),(gr1 `2)]| = g . r2
by A120, A121, A122, A126, EUCLID:53;
then
g . r1 = g . r2
by EUCLID:53;
hence
x1 = x2
by A93, A94, FUNCT_1:def 4;
verum end; case A127:
(
g . r1 in LSeg (
|[b,d]|,
|[b,c]|) &
g . r2 in LSeg (
|[b,c]|,
|[a,c]|) )
;
x1 = x2then A128:
gr1 `1 = b
by A2, Th1;
A129:
c <= gr1 `2
by A2, A127, Th1;
A130:
gr2 `2 = c
by A1, A127, Th3;
A131:
gr2 `1 <= b
by A1, A127, Th3;
A132:
b + (gr1 `2) = (gr2 `1) + c
by A2, A120, A121, A122, A127, A130, Th1;
then
|[(gr1 `1),(gr1 `2)]| = g . r2
by A128, A130, A133, EUCLID:53;
then
g . r1 = g . r2
by EUCLID:53;
hence
x1 = x2
by A93, A94, FUNCT_1:def 4;
verum end; case A134:
(
g . r1 in LSeg (
|[b,c]|,
|[a,c]|) &
g . r2 in LSeg (
|[b,d]|,
|[b,c]|) )
;
x1 = x2then A135:
gr2 `1 = b
by A2, Th1;
A136:
c <= gr2 `2
by A2, A134, Th1;
A137:
gr1 `2 = c
by A1, A134, Th3;
A138:
gr1 `1 <= b
by A1, A134, Th3;
A139:
b + (gr2 `2) = (gr1 `1) + c
by A1, A120, A121, A122, A134, A135, Th3;
then
|[(gr2 `1),(gr2 `2)]| = g . r1
by A135, A137, A140, EUCLID:53;
then
g . r1 = g . r2
by EUCLID:53;
hence
x1 = x2
by A93, A94, FUNCT_1:def 4;
verum end; case A141:
(
g . r1 in LSeg (
|[b,c]|,
|[a,c]|) &
g . r2 in LSeg (
|[b,c]|,
|[a,c]|) )
;
x1 = x2then A142:
gr1 `2 = c
by A1, Th3;
gr2 `2 = c
by A1, A141, Th3;
then
|[(gr1 `1),(gr1 `2)]| = g . r2
by A120, A121, A122, A142, EUCLID:53;
then
g . r1 = g . r2
by EUCLID:53;
hence
x1 = x2
by A93, A94, FUNCT_1:def 4;
verum end; end; end;
hence
x1 = x2
;
verum
end; A143:
dom k = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
then
s1 in dom k
by A88, A89, XXREAL_1:1;
then
rxc = s1
by A111, A115, A116, A117, A143;
hence
contradiction
by A102, A115, XXREAL_1:1;
verum end;
hence
s1 <= s2
;
verum
end; then
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 A83, A84, JORDAN5C:def 3;
hence
LE p1,
p2,
rectangle (
a,
b,
c,
d)
by A79, A83, A84, JORDAN6:def 10;
verum end; end; end;
hence
LE p1,
p2,
rectangle (
a,
b,
c,
d)
;
verum
end;