A1:
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;
A2:
[#] I[01] is compact
by COMPTS_1:1;
let P, Q be non empty Subset of (TOP-REAL 2); for p1, p2, q1, q2 being Point of (TOP-REAL 2)
for f being Path of p1,p2
for g being Path of q1,q2 st rng f = P & rng g = Q & ( for p being Point of (TOP-REAL 2) st p in P holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) holds
P meets Q
let p1, p2, q1, q2 be Point of (TOP-REAL 2); for f being Path of p1,p2
for g being Path of q1,q2 st rng f = P & rng g = Q & ( for p being Point of (TOP-REAL 2) st p in P holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) holds
P meets Q
let f be Path of p1,p2; for g being Path of q1,q2 st rng f = P & rng g = Q & ( for p being Point of (TOP-REAL 2) st p in P holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) holds
P meets Q
let g be Path of q1,q2; ( rng f = P & rng g = Q & ( for p being Point of (TOP-REAL 2) st p in P holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) implies P meets Q )
assume that
A3:
rng f = P
and
A4:
rng g = Q
and
A5:
for p being Point of (TOP-REAL 2) st p in P holds
( p1 `1 <= p `1 & p `1 <= p2 `1 )
and
A6:
for p being Point of (TOP-REAL 2) st p in Q holds
( p1 `1 <= p `1 & p `1 <= p2 `1 )
and
A7:
for p being Point of (TOP-REAL 2) st p in P holds
( q1 `2 <= p `2 & p `2 <= q2 `2 )
and
A8:
for p being Point of (TOP-REAL 2) st p in Q holds
( q1 `2 <= p `2 & p `2 <= q2 `2 )
; P meets Q
TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #)
by EUCLID:def 8;
then reconsider P9 = P, Q9 = Q as Subset of (TopSpaceMetr (Euclid 2)) ;
set e = (min_dist_min (P9,Q9)) / 5;
f .: the carrier of I[01] = rng f
by RELSET_1:22;
then
P is compact
by A3, A2, WEIERSTR:8;
then A9:
P9 is compact
by A1, COMPTS_1:23;
g .: ([#] I[01]) = rng g
by RELSET_1:22;
then
Q is compact
by A4, A2, WEIERSTR:8;
then A10:
Q9 is compact
by A1, COMPTS_1:23;
assume A11:
P /\ Q = {}
; XBOOLE_0:def 7 contradiction
then
P misses Q
;
then A12:
min_dist_min (P9,Q9) > 0
by A10, A9, JGRAPH_1:38;
then A13:
(min_dist_min (P9,Q9)) / 5 > 0 / 5
by XREAL_1:74;
then consider h being FinSequence of REAL such that
A14:
h . 1 = 0
and
A15:
h . (len h) = 1
and
A16:
5 <= len h
and
A17:
rng h c= the carrier of I[01]
and
A18:
h is increasing
and
A19:
for i being Nat
for R being Subset of I[01]
for W being Subset of (Euclid 2) st 1 <= i & i < len h & R = [.(h /. i),(h /. (i + 1)).] & W = f .: R holds
diameter W < (min_dist_min (P9,Q9)) / 5
by Th1;
deffunc H1( Nat) -> set = f . (h . $1);
ex h19 being FinSequence st
( len h19 = len h & ( for i being Nat st i in dom h19 holds
h19 . i = H1(i) ) )
from FINSEQ_1:sch 2();
then consider h19 being FinSequence such that
A20:
len h19 = len h
and
A21:
for i being Nat st i in dom h19 holds
h19 . i = f . (h . i)
;
A22:
1 <= len h
by A16, XXREAL_0:2;
then A23:
len h in dom h19
by A20, FINSEQ_3:25;
rng h19 c= the carrier of (TOP-REAL 2)
then reconsider h1 = h19 as FinSequence of (TOP-REAL 2) by FINSEQ_1:def 4;
A28:
len h1 >= 1
by A16, A20, XXREAL_0:2;
then A29:
h1 . 1 = h1 /. 1
by FINSEQ_4:15;
A30:
f . 0 = p1
by BORSUK_2:def 4;
A31:
for i being Nat st 1 <= i & i + 1 <= len h1 holds
|.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
proof
reconsider Pa =
P as
Subset of
(TOP-REAL 2) ;
A32:
dom f = the
carrier of
I[01]
by FUNCT_2:def 1;
reconsider W1 =
P as
Subset of
(Euclid 2) by TOPREAL3:8;
let i be
Nat;
( 1 <= i & i + 1 <= len h1 implies |.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 )
assume that A33:
1
<= i
and A34:
i + 1
<= len h1
;
|.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
A35:
1
< i + 1
by A33, NAT_1:13;
then A36:
h . (i + 1) = h /. (i + 1)
by A20, A34, FINSEQ_4:15;
A37:
i + 1
in dom h19
by A34, A35, FINSEQ_3:25;
then A38:
h19 . (i + 1) = f . (h . (i + 1))
by A21;
then A39:
h1 /. (i + 1) = f . (h . (i + 1))
by A34, A35, FINSEQ_4:15;
set r1 =
(((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1;
(
[#] I[01] is
compact &
f .: the
carrier of
I[01] = rng f )
by COMPTS_1:1, RELSET_1:22;
then A40:
Pa is
compact
by A3, WEIERSTR:8;
A41:
for
x,
y being
Point of
(Euclid 2) st
x in W1 &
y in W1 holds
dist (
x,
y)
<= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1
proof
let x,
y be
Point of
(Euclid 2);
( x in W1 & y in W1 implies dist (x,y) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1 )
assume that A42:
x in W1
and A43:
y in W1
;
dist (x,y) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1
reconsider pw1 =
x,
pw2 =
y as
Point of
(TOP-REAL 2) by A42, A43;
A44:
(
S-bound Pa <= pw2 `2 &
pw2 `2 <= N-bound Pa )
by A40, A43, PSCOMP_1:24;
(
S-bound Pa <= pw1 `2 &
pw1 `2 <= N-bound Pa )
by A40, A42, PSCOMP_1:24;
then A45:
|.((pw1 `2) - (pw2 `2)).| <= (N-bound Pa) - (S-bound Pa)
by A44, JGRAPH_1:27;
A46:
((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa)) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1
by XREAL_1:29;
A47:
(
W-bound Pa <= pw2 `1 &
pw2 `1 <= E-bound Pa )
by A40, A43, PSCOMP_1:24;
(
W-bound Pa <= pw1 `1 &
pw1 `1 <= E-bound Pa )
by A40, A42, PSCOMP_1:24;
then
|.((pw1 `1) - (pw2 `1)).| <= (E-bound Pa) - (W-bound Pa)
by A47, JGRAPH_1:27;
then
|.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= ((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))
by A45, XREAL_1:7;
then A48:
|.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1
by A46, XXREAL_0:2;
(
dist (
x,
y)
= |.(pw1 - pw2).| &
|.(pw1 - pw2).| <= |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| )
by JGRAPH_1:28, JGRAPH_1:32;
hence
dist (
x,
y)
<= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1
by A48, XXREAL_0:2;
verum
end;
i + 1
in dom h
by A20, A34, A35, FINSEQ_3:25;
then
h . (i + 1) in rng h
by FUNCT_1:def 3;
then
h19 . (i + 1) in rng f
by A17, A38, A32, FUNCT_1:def 3;
then A49:
f . (h . (i + 1)) is
Element of
(TOP-REAL 2)
by A21, A37;
A50:
i < len h1
by A34, NAT_1:13;
then A51:
h . i = h /. i
by A20, A33, FINSEQ_4:15;
A52:
i in dom h
by A20, A33, A50, FINSEQ_3:25;
then A53:
h . i in rng h
by FUNCT_1:def 3;
A54:
i + 1
in dom h
by A20, A34, A35, FINSEQ_3:25;
then
h . (i + 1) in rng h
by FUNCT_1:def 3;
then reconsider R =
[.(h /. i),(h /. (i + 1)).] as
Subset of
I[01] by A17, A53, A51, A36, BORSUK_1:40, XXREAL_2:def 12;
A55:
i in dom h19
by A33, A50, FINSEQ_3:25;
then A56:
h19 . i = f . (h . i)
by A21;
then
h19 . i in rng f
by A17, A53, A32, FUNCT_1:def 3;
then
f . (h . i) is
Element of
(TOP-REAL 2)
by A21, A55;
then reconsider w1 =
f . (h . i),
w2 =
f . (h . (i + 1)) as
Point of
(Euclid 2) by A49, TOPREAL3:8;
i < i + 1
by NAT_1:13;
then A57:
h /. i <= h /. (i + 1)
by A18, A52, A51, A54, A36, SEQM_3:def 1;
then
h . i in R
by A51, XXREAL_1:1;
then A58:
w1 in f .: R
by A32, FUNCT_1:def 6;
0 in the
carrier of
I[01]
by BORSUK_1:43;
then A59:
f . 0 in rng f
by A32, FUNCT_1:def 3;
then
(
S-bound Pa <= p1 `2 &
p1 `2 <= N-bound Pa )
by A3, A30, A40, PSCOMP_1:24;
then
S-bound Pa <= N-bound Pa
by XXREAL_0:2;
then A60:
0 <= (N-bound Pa) - (S-bound Pa)
by XREAL_1:48;
(
W-bound Pa <= p1 `1 &
p1 `1 <= E-bound Pa )
by A3, A30, A40, A59, PSCOMP_1:24;
then
W-bound Pa <= E-bound Pa
by XXREAL_0:2;
then
0 <= (E-bound Pa) - (W-bound Pa)
by XREAL_1:48;
then A61:
W1 is
bounded
by A60, A41, TBSP_1:def 7;
h . (i + 1) in R
by A36, A57, XXREAL_1:1;
then A62:
w2 in f .: R
by A32, FUNCT_1:def 6;
reconsider W =
f .: R as
Subset of
(Euclid 2) by TOPREAL3:8;
dom f = [#] I[01]
by FUNCT_2:def 1;
then
P = f .: [.0,1.]
by A3, BORSUK_1:40, RELAT_1:113;
then
W is
bounded
by A61, BORSUK_1:40, RELAT_1:123, TBSP_1:14;
then A63:
dist (
w1,
w2)
<= diameter W
by A58, A62, TBSP_1:def 8;
diameter W < (min_dist_min (P9,Q9)) / 5
by A19, A20, A33, A50;
then A64:
dist (
w1,
w2)
< (min_dist_min (P9,Q9)) / 5
by A63, XXREAL_0:2;
h1 /. i = f . (h . i)
by A33, A50, A56, FINSEQ_4:15;
hence
|.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
by A39, A64, JGRAPH_1:28;
verum
end;
A65:
for i being Nat st i in dom h1 holds
( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 )
for i being Nat st i in dom (Y_axis h1) holds
( q1 `2 <= (Y_axis h1) . i & (Y_axis h1) . i <= q2 `2 )
then A70:
Y_axis h1 lies_between q1 `2 ,q2 `2
by GOBOARD4:def 2;
A71:
f . 1 = p2
by BORSUK_2:def 4;
A72:
for i being Nat st i in dom h1 holds
( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 )
proof
len h in dom h19
by A20, A28, FINSEQ_3:25;
then
h1 . (len h1) = f . (h . (len h))
by A20, A21;
then A73:
h1 /. (len h1) = f . (h . (len h))
by A28, FINSEQ_4:15;
1
in dom h19
by A28, FINSEQ_3:25;
then
h1 . 1
= f . (h . 1)
by A21;
then A74:
h1 /. 1
= f . (h . 1)
by A28, FINSEQ_4:15;
let i be
Nat;
( i in dom h1 implies ( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 ) )
assume A75:
i in dom h1
;
( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 )
then
h1 . i = f . (h . i)
by A21;
then A76:
h1 /. i = f . (h . i)
by A75, PARTFUN1:def 6;
i in dom h
by A20, A75, FINSEQ_3:29;
then A77:
h . i in rng h
by FUNCT_1:def 3;
dom f = the
carrier of
I[01]
by FUNCT_2:def 1;
then
h1 /. i in rng f
by A17, A76, A77, FUNCT_1:def 3;
hence
(
(h1 /. 1) `1 <= (h1 /. i) `1 &
(h1 /. i) `1 <= (h1 /. (len h1)) `1 )
by A3, A5, A30, A71, A14, A15, A74, A73;
verum
end;
for i being Nat st i in dom (X_axis h1) holds
( (X_axis h1) . 1 <= (X_axis h1) . i & (X_axis h1) . i <= (X_axis h1) . (len h1) )
then
X_axis h1 lies_between (X_axis h1) . 1,(X_axis h1) . (len h1)
by GOBOARD4:def 2;
then consider f2 being FinSequence of (TOP-REAL 2) such that
A80:
f2 is special
and
A81:
f2 . 1 = h1 . 1
and
A82:
f2 . (len f2) = h1 . (len h1)
and
A83:
len f2 >= len h1
and
A84:
( X_axis f2 lies_between (X_axis h1) . 1,(X_axis h1) . (len h1) & Y_axis f2 lies_between q1 `2 ,q2 `2 )
and
A85:
for j being Nat st j in dom f2 holds
ex k being Nat st
( k in dom h1 & |.((f2 /. j) - (h1 /. k)).| < (min_dist_min (P9,Q9)) / 5 )
and
A86:
for j being Nat st 1 <= j & j + 1 <= len f2 holds
|.((f2 /. j) - (f2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5
by A13, A31, A28, A70, JGRAPH_1:39;
A87:
len f2 >= 1
by A28, A83, XXREAL_0:2;
then A88:
f2 . (len f2) = f2 /. (len f2)
by FINSEQ_4:15;
consider hb being FinSequence of REAL such that
A89:
hb . 1 = 0
and
A90:
hb . (len hb) = 1
and
A91:
5 <= len hb
and
A92:
rng hb c= the carrier of I[01]
and
A93:
hb is increasing
and
A94:
for i being Nat
for R being Subset of I[01]
for W being Subset of (Euclid 2) st 1 <= i & i < len hb & R = [.(hb /. i),(hb /. (i + 1)).] & W = g .: R holds
diameter W < (min_dist_min (P9,Q9)) / 5
by A13, Th1;
deffunc H2( Nat) -> set = g . (hb . $1);
ex h29 being FinSequence st
( len h29 = len hb & ( for i being Nat st i in dom h29 holds
h29 . i = H2(i) ) )
from FINSEQ_1:sch 2();
then consider h29 being FinSequence such that
A95:
len h29 = len hb
and
A96:
for i being Nat st i in dom h29 holds
h29 . i = g . (hb . i)
;
rng h29 c= the carrier of (TOP-REAL 2)
then reconsider h2 = h29 as FinSequence of (TOP-REAL 2) by FINSEQ_1:def 4;
A101:
len h2 >= 1
by A91, A95, XXREAL_0:2;
1 in dom h19
by A20, A22, FINSEQ_3:25;
then A102:
h1 /. 1 = f . (h . 1)
by A21, A29;
A103:
0 in the carrier of I[01]
by BORSUK_1:43;
then
0 in dom f
by FUNCT_2:def 1;
then A104:
p1 in P9
by A3, A30, FUNCT_1:def 3;
A105:
1 <= len hb
by A91, XXREAL_0:2;
then A106:
h2 . (len h2) = h2 /. (len h2)
by A95, FINSEQ_4:15;
A107:
g . 0 = q1
by BORSUK_2:def 4;
A108:
for i being Nat st 1 <= i & i + 1 <= len h2 holds
|.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
proof
reconsider Qa =
Q as
Subset of
(TOP-REAL 2) ;
A109:
dom g = the
carrier of
I[01]
by FUNCT_2:def 1;
reconsider W1 =
Q as
Subset of
(Euclid 2) by TOPREAL3:8;
let i be
Nat;
( 1 <= i & i + 1 <= len h2 implies |.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 )
assume that A110:
1
<= i
and A111:
i + 1
<= len h2
;
|.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
A112:
i < len h2
by A111, NAT_1:13;
then A113:
hb . i = hb /. i
by A95, A110, FINSEQ_4:15;
A114:
1
< i + 1
by A110, NAT_1:13;
then
i + 1
in Seg (len hb)
by A95, A111, FINSEQ_1:1;
then
i + 1
in dom hb
by FINSEQ_1:def 3;
then A115:
hb . (i + 1) in rng hb
by FUNCT_1:def 3;
A116:
i + 1
in dom h29
by A111, A114, FINSEQ_3:25;
then
h29 . (i + 1) = g . (hb . (i + 1))
by A96;
then
h29 . (i + 1) in rng g
by A92, A109, A115, FUNCT_1:def 3;
then A117:
g . (hb . (i + 1)) is
Element of
(TOP-REAL 2)
by A96, A116;
i in dom h29
by A110, A112, FINSEQ_3:25;
then A118:
h29 . i = g . (hb . i)
by A96;
(
[#] I[01] is
compact &
g .: the
carrier of
I[01] = rng g )
by COMPTS_1:1, RELSET_1:22;
then A119:
Qa is
compact
by A4, WEIERSTR:8;
reconsider Qa =
Qa as non
empty Subset of
(TOP-REAL 2) ;
set r1 =
(((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1;
A120:
hb . (i + 1) = hb /. (i + 1)
by A95, A111, A114, FINSEQ_4:15;
A121:
for
x,
y being
Point of
(Euclid 2) st
x in W1 &
y in W1 holds
dist (
x,
y)
<= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1
proof
let x,
y be
Point of
(Euclid 2);
( x in W1 & y in W1 implies dist (x,y) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1 )
assume that A122:
x in W1
and A123:
y in W1
;
dist (x,y) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1
reconsider pw1 =
x,
pw2 =
y as
Point of
(TOP-REAL 2) by A122, A123;
A124:
(
S-bound Qa <= pw2 `2 &
pw2 `2 <= N-bound Qa )
by A119, A123, PSCOMP_1:24;
(
S-bound Qa <= pw1 `2 &
pw1 `2 <= N-bound Qa )
by A119, A122, PSCOMP_1:24;
then A125:
|.((pw1 `2) - (pw2 `2)).| <= (N-bound Qa) - (S-bound Qa)
by A124, JGRAPH_1:27;
A126:
((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa)) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1
by XREAL_1:29;
A127:
(
W-bound Qa <= pw2 `1 &
pw2 `1 <= E-bound Qa )
by A119, A123, PSCOMP_1:24;
(
W-bound Qa <= pw1 `1 &
pw1 `1 <= E-bound Qa )
by A119, A122, PSCOMP_1:24;
then
|.((pw1 `1) - (pw2 `1)).| <= (E-bound Qa) - (W-bound Qa)
by A127, JGRAPH_1:27;
then
|.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= ((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))
by A125, XREAL_1:7;
then A128:
|.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1
by A126, XXREAL_0:2;
(
dist (
x,
y)
= |.(pw1 - pw2).| &
|.(pw1 - pw2).| <= |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| )
by JGRAPH_1:28, JGRAPH_1:32;
hence
dist (
x,
y)
<= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1
by A128, XXREAL_0:2;
verum
end;
0 in the
carrier of
I[01]
by BORSUK_1:43;
then A129:
g . 0 in rng g
by A109, FUNCT_1:def 3;
then
(
S-bound Qa <= q1 `2 &
q1 `2 <= N-bound Qa )
by A4, A107, A119, PSCOMP_1:24;
then
S-bound Qa <= N-bound Qa
by XXREAL_0:2;
then A130:
0 <= (N-bound Qa) - (S-bound Qa)
by XREAL_1:48;
i in Seg (len hb)
by A95, A110, A112, FINSEQ_1:1;
then A131:
i in dom hb
by FINSEQ_1:def 3;
then A132:
hb . i in rng hb
by FUNCT_1:def 3;
then
h29 . i in rng g
by A92, A118, A109, FUNCT_1:def 3;
then reconsider w1 =
g . (hb . i),
w2 =
g . (hb . (i + 1)) as
Point of
(Euclid 2) by A118, A117, TOPREAL3:8;
i + 1
in Seg (len hb)
by A95, A111, A114, FINSEQ_1:1;
then A133:
i + 1
in dom hb
by FINSEQ_1:def 3;
then
hb . (i + 1) in rng hb
by FUNCT_1:def 3;
then reconsider R =
[.(hb /. i),(hb /. (i + 1)).] as
Subset of
I[01] by A92, A132, A113, A120, BORSUK_1:40, XXREAL_2:def 12;
i < i + 1
by NAT_1:13;
then A134:
hb /. i <= hb /. (i + 1)
by A93, A131, A113, A133, A120, SEQM_3:def 1;
then
hb . i in R
by A113, XXREAL_1:1;
then A135:
w1 in g .: R
by A109, FUNCT_1:def 6;
(
W-bound Qa <= q1 `1 &
q1 `1 <= E-bound Qa )
by A4, A107, A119, A129, PSCOMP_1:24;
then
W-bound Qa <= E-bound Qa
by XXREAL_0:2;
then
0 <= (E-bound Qa) - (W-bound Qa)
by XREAL_1:48;
then A136:
W1 is
bounded
by A130, A121, TBSP_1:def 7;
hb . (i + 1) in R
by A120, A134, XXREAL_1:1;
then A137:
w2 in g .: R
by A109, FUNCT_1:def 6;
reconsider W =
g .: R as
Subset of
(Euclid 2) by TOPREAL3:8;
dom g = [#] I[01]
by FUNCT_2:def 1;
then
Q = g .: [.0,1.]
by A4, BORSUK_1:40, RELAT_1:113;
then
W is
bounded
by A136, BORSUK_1:40, RELAT_1:123, TBSP_1:14;
then A138:
dist (
w1,
w2)
<= diameter W
by A135, A137, TBSP_1:def 8;
diameter W < (min_dist_min (P9,Q9)) / 5
by A94, A95, A110, A112;
then A139:
dist (
w1,
w2)
< (min_dist_min (P9,Q9)) / 5
by A138, XXREAL_0:2;
h2 . (i + 1) = h2 /. (i + 1)
by A111, A114, FINSEQ_4:15;
then A140:
h2 /. (i + 1) = g . (hb . (i + 1))
by A96, A116;
h2 /. i = g . (hb . i)
by A110, A112, A118, FINSEQ_4:15;
hence
|.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
by A140, A139, JGRAPH_1:28;
verum
end;
A141:
dom hb = Seg (len hb)
by FINSEQ_1:def 3;
A142:
for i being Nat st i in dom hb holds
h2 /. i = g . (hb . i)
A145:
for i being Nat st i in dom h2 holds
( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 )
for i being Nat st i in dom (X_axis h2) holds
( p1 `1 <= (X_axis h2) . i & (X_axis h2) . i <= p2 `1 )
then A148:
X_axis h2 lies_between p1 `1 ,p2 `1
by GOBOARD4:def 2;
A149:
g . 1 = q2
by BORSUK_2:def 4;
A150:
for i being Nat st i in dom h2 holds
( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 )
proof
let i be
Nat;
( i in dom h2 implies ( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 ) )
assume
i in dom h2
;
( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 )
then
i in Seg (len h2)
by FINSEQ_1:def 3;
then
i in dom hb
by A95, FINSEQ_1:def 3;
then A151:
(
h2 /. i = g . (hb . i) &
hb . i in rng hb )
by A142, FUNCT_1:def 3;
1
in Seg (len hb)
by A95, A101, FINSEQ_1:1;
then
1
in dom hb
by FINSEQ_1:def 3;
then A152:
h2 /. 1
= g . (hb . 1)
by A142;
len hb in Seg (len hb)
by A95, A101, FINSEQ_1:1;
then
len hb in dom hb
by FINSEQ_1:def 3;
then A153:
h2 /. (len h2) = g . (hb . (len hb))
by A95, A142;
dom g = the
carrier of
I[01]
by FUNCT_2:def 1;
then
h2 /. i in rng g
by A92, A151, FUNCT_1:def 3;
hence
(
(h2 /. 1) `2 <= (h2 /. i) `2 &
(h2 /. i) `2 <= (h2 /. (len h2)) `2 )
by A4, A8, A107, A149, A89, A90, A152, A153;
verum
end;
for i being Nat st i in dom (Y_axis h2) holds
( (Y_axis h2) . 1 <= (Y_axis h2) . i & (Y_axis h2) . i <= (Y_axis h2) . (len h2) )
then
Y_axis h2 lies_between (Y_axis h2) . 1,(Y_axis h2) . (len h2)
by GOBOARD4:def 2;
then consider g2 being FinSequence of (TOP-REAL 2) such that
A156:
g2 is special
and
A157:
g2 . 1 = h2 . 1
and
A158:
g2 . (len g2) = h2 . (len h2)
and
A159:
len g2 >= len h2
and
A160:
( Y_axis g2 lies_between (Y_axis h2) . 1,(Y_axis h2) . (len h2) & X_axis g2 lies_between p1 `1 ,p2 `1 )
and
A161:
for j being Nat st j in dom g2 holds
ex k being Nat st
( k in dom h2 & |.((g2 /. j) - (h2 /. k)).| < (min_dist_min (P9,Q9)) / 5 )
and
A162:
for j being Nat st 1 <= j & j + 1 <= len g2 holds
|.((g2 /. j) - (g2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5
by A13, A101, A148, A108, JGRAPH_1:40;
A163:
len g2 >= 1
by A101, A159, XXREAL_0:2;
then A164:
g2 /. (len g2) = g2 . (len g2)
by FINSEQ_4:15;
1 in dom hb
by A105, FINSEQ_3:25;
then A165:
h2 /. 1 = q1
by A107, A89, A142;
A166:
h2 . 1 = h2 /. 1
by A105, A95, FINSEQ_4:15;
A167:
h1 . (len h1) = h1 /. (len h1)
by A28, FINSEQ_4:15;
then A168: (X_axis f2) . (len f2) =
(h1 /. (len h1)) `1
by A82, A87, A88, JGRAPH_1:41
.=
(X_axis h1) . (len h1)
by A28, JGRAPH_1:41
;
len h in dom h19
by A20, A28, FINSEQ_3:25;
then
h1 /. (len h1) = p2
by A71, A15, A20, A21, A167;
then A169:
(X_axis f2) . (len f2) = p2 `1
by A82, A87, A167, A88, JGRAPH_1:41;
5 <= len f2
by A16, A20, A83, XXREAL_0:2;
then A170:
2 <= len f2
by XXREAL_0:2;
0 in dom g
by A103, FUNCT_2:def 1;
then A171:
q1 in Q9
by A4, A107, FUNCT_1:def 3;
A172:
f2 . 1 = f2 /. 1
by A87, FINSEQ_4:15;
g2 . 1 = g2 /. 1
by A163, FINSEQ_4:15;
then A173: (Y_axis g2) . 1 =
(h2 /. 1) `2
by A157, A163, A166, JGRAPH_1:42
.=
(Y_axis h2) . 1
by A101, JGRAPH_1:42
;
g2 /. 1 = g2 . 1
by A163, FINSEQ_4:15;
then A174:
(Y_axis g2) . 1 = q1 `2
by A157, A163, A165, A166, JGRAPH_1:42;
len hb in dom hb
by A105, FINSEQ_3:25;
then
g2 . (len g2) = q2
by A149, A90, A95, A142, A158, A106;
then A175:
(Y_axis g2) . (len g2) = q2 `2
by A163, A164, JGRAPH_1:42;
g2 . (len g2) = g2 /. (len g2)
by A163, FINSEQ_4:15;
then A176: (Y_axis g2) . (len g2) =
(h2 /. (len h2)) `2
by A158, A163, A106, JGRAPH_1:42
.=
(Y_axis h2) . (len h2)
by A101, JGRAPH_1:42
;
5 <= len g2
by A91, A95, A159, XXREAL_0:2;
then A177:
2 <= len g2
by XXREAL_0:2;
1 in dom h19
by A28, FINSEQ_3:25;
then
h1 . 1 = f . (h . 1)
by A21;
then A178:
(X_axis f2) . 1 = p1 `1
by A30, A14, A81, A87, A172, JGRAPH_1:41;
A179: (X_axis f2) . 1 =
(h1 /. 1) `1
by A81, A87, A29, A172, JGRAPH_1:41
.=
(X_axis h1) . 1
by A28, JGRAPH_1:41
;
now ( ( p1 = p2 & contradiction ) or ( p1 <> p2 & contradiction ) )per cases
( p1 = p2 or p1 <> p2 )
;
case A180:
p1 = p2
;
contradiction
0 in the
carrier of
I[01]
by BORSUK_1:43;
then
0 in dom f
by FUNCT_2:def 1;
then A181:
p1 in P
by A3, A30, FUNCT_1:3;
0 in the
carrier of
I[01]
by BORSUK_1:43;
then A182:
0 in dom g
by FUNCT_2:def 1;
then A183:
q1 in Q
by A4, A107, FUNCT_1:3;
A184:
for
q being
Point of
(TOP-REAL 2) st
q in Q holds
q `1 = p1 `1
A185:
now not q1 `2 = q2 `2 assume A186:
q1 `2 = q2 `2
;
contradiction
(
q1 `2 <= p1 `2 &
p1 `2 <= q2 `2 )
by A7, A181;
then A187:
p1 `2 = q1 `2
by A186, XXREAL_0:1;
q1 `1 = p1 `1
by A4, A107, A184, A182, FUNCT_1:3;
then
q1 = p1
by A187, TOPREAL3:6;
hence
contradiction
by A11, A183, A181, XBOOLE_0:def 4;
verum end; A188:
p1 in LSeg (
q1,
q2)
proof
1
in the
carrier of
I[01]
by BORSUK_1:43;
then
1
in dom g
by FUNCT_2:def 1;
then
g . 1
in rng g
by FUNCT_1:3;
then
(
p1 `1 <= q2 `1 &
q2 `1 <= p2 `1 )
by A4, A6, A149;
then A189:
p1 `1 = q2 `1
by A180, XXREAL_0:1;
set ln =
((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2));
A190:
(((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (q2 `2) =
(((p1 `2) - (q1 `2)) * (q2 `2)) / ((q2 `2) - (q1 `2))
by XCMPLX_1:74
.=
(((p1 `2) * (q2 `2)) - ((q1 `2) * (q2 `2))) / ((q2 `2) - (q1 `2))
;
A191:
(q2 `2) - (q1 `2) <> 0
by A185;
then 1
- (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) =
(((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))
by XCMPLX_1:60
.=
(((q2 `2) - (q1 `2)) - ((p1 `2) - (q1 `2))) / ((q2 `2) - (q1 `2))
by XCMPLX_1:120
.=
((q2 `2) - (p1 `2)) / ((q2 `2) - (q1 `2))
;
then A192:
(1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2) =
(((q2 `2) - (p1 `2)) * (q1 `2)) / ((q2 `2) - (q1 `2))
by XCMPLX_1:74
.=
(((q2 `2) * (q1 `2)) - ((p1 `2) * (q1 `2))) / ((q2 `2) - (q1 `2))
;
0 in the
carrier of
I[01]
by BORSUK_1:43;
then
0 in dom g
by FUNCT_2:def 1;
then
q1 in Q
by A4, A107, FUNCT_1:3;
then
(
p1 `1 <= q1 `1 &
q1 `1 <= p2 `1 )
by A6;
then A193:
p1 `1 = q1 `1
by A180, XXREAL_0:1;
0 in the
carrier of
I[01]
by BORSUK_1:43;
then
0 in dom f
by FUNCT_2:def 1;
then A194:
f . 0 in rng f
by FUNCT_1:3;
then A195:
q1 `2 <= p1 `2
by A3, A7, A30;
A196:
(((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2)) `1 =
(((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) `1) + (((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `1)
by TOPREAL3:2
.=
((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `1)) + (((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `1)
by TOPREAL3:4
.=
((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (p1 `1)) + ((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (p1 `1))
by A193, A189, TOPREAL3:4
.=
p1 `1
;
(((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2)) `2 =
(((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) `2) + (((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `2)
by TOPREAL3:2
.=
((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2)) + (((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `2)
by TOPREAL3:4
.=
((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2)) + ((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (q2 `2))
by TOPREAL3:4
.=
((((q2 `2) * (q1 `2)) - ((p1 `2) * (q1 `2))) + (((p1 `2) * (q2 `2)) - ((q1 `2) * (q2 `2)))) / ((q2 `2) - (q1 `2))
by A192, A190, XCMPLX_1:62
.=
((p1 `2) * ((q2 `2) - (q1 `2))) / ((q2 `2) - (q1 `2))
.=
(p1 `2) * (((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))
by XCMPLX_1:74
.=
(p1 `2) * 1
by A191, XCMPLX_1:60
.=
p1 `2
;
then A197:
((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) = p1
by A196, TOPREAL3:6;
A198:
p1 `2 <= q2 `2
by A3, A7, A30, A194;
then
q2 `2 >= q1 `2
by A195, XXREAL_0:2;
then
q2 `2 > q1 `2
by A185, XXREAL_0:1;
then A199:
(q2 `2) - (q1 `2) > 0
by XREAL_1:50;
(p1 `2) - (q1 `2) <= (q2 `2) - (q1 `2)
by A198, XREAL_1:13;
then
((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) <= ((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))
by A199, XREAL_1:72;
then A200:
((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) <= 1
by A199, XCMPLX_1:60;
(p1 `2) - (q1 `2) >= 0
by A195, XREAL_1:48;
hence
p1 in LSeg (
q1,
q2)
by A199, A200, A197;
verum
end;
1
in the
carrier of
I[01]
by BORSUK_1:43;
then
1
in dom g
by FUNCT_2:def 1;
then A201:
q2 in Q
by A4, A149, FUNCT_1:3;
Q c= LSeg (
q1,
q2)
proof
(
p1 `1 <= q2 `1 &
q2 `1 <= p2 `1 )
by A6, A201;
then A202:
p1 `1 = q2 `1
by A180, XXREAL_0:1;
(
p1 `1 <= q1 `1 &
q1 `1 <= p2 `1 )
by A6, A183;
then A203:
p1 `1 = q1 `1
by A180, XXREAL_0:1;
let z be
object ;
TARSKI:def 3 ( not z in Q or z in LSeg (q1,q2) )
assume A204:
z in Q
;
z in LSeg (q1,q2)
then reconsider qz =
z as
Point of
(TOP-REAL 2) ;
A205:
qz `2 <= q2 `2
by A8, A204;
set ln =
((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2));
A206:
(((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (q2 `2) =
(((qz `2) - (q1 `2)) * (q2 `2)) / ((q2 `2) - (q1 `2))
by XCMPLX_1:74
.=
(((qz `2) * (q2 `2)) - ((q1 `2) * (q2 `2))) / ((q2 `2) - (q1 `2))
;
A207:
(q2 `2) - (q1 `2) <> 0
by A185;
then 1
- (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) =
(((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))
by XCMPLX_1:60
.=
(((q2 `2) - (q1 `2)) - ((qz `2) - (q1 `2))) / ((q2 `2) - (q1 `2))
by XCMPLX_1:120
.=
((q2 `2) - (qz `2)) / ((q2 `2) - (q1 `2))
;
then A208:
(1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2) =
(((q2 `2) - (qz `2)) * (q1 `2)) / ((q2 `2) - (q1 `2))
by XCMPLX_1:74
.=
(((q2 `2) * (q1 `2)) - ((qz `2) * (q1 `2))) / ((q2 `2) - (q1 `2))
;
A209:
(((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2)) `2 =
(((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) `2) + (((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `2)
by TOPREAL3:2
.=
((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2)) + (((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `2)
by TOPREAL3:4
.=
((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2)) + ((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (q2 `2))
by TOPREAL3:4
.=
((((q2 `2) * (q1 `2)) - ((qz `2) * (q1 `2))) + (((qz `2) * (q2 `2)) - ((q1 `2) * (q2 `2)))) / ((q2 `2) - (q1 `2))
by A208, A206, XCMPLX_1:62
.=
((qz `2) * ((q2 `2) - (q1 `2))) / ((q2 `2) - (q1 `2))
.=
(qz `2) * (((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))
by XCMPLX_1:74
.=
(qz `2) * 1
by A207, XCMPLX_1:60
.=
qz `2
;
A210:
(
p1 `1 <= qz `1 &
qz `1 <= p2 `1 )
by A6, A204;
(((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2)) `1 =
(((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) `1) + (((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `1)
by TOPREAL3:2
.=
((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `1)) + (((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `1)
by TOPREAL3:4
.=
((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (p1 `1)) + ((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (p1 `1))
by A203, A202, TOPREAL3:4
.=
qz `1
by A180, A210, XXREAL_0:1
;
then A211:
((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) = qz
by A209, TOPREAL3:6;
A212:
q1 `2 <= qz `2
by A8, A204;
then
q2 `2 >= q1 `2
by A205, XXREAL_0:2;
then
q2 `2 > q1 `2
by A185, XXREAL_0:1;
then A213:
(q2 `2) - (q1 `2) > 0
by XREAL_1:50;
(qz `2) - (q1 `2) <= (q2 `2) - (q1 `2)
by A205, XREAL_1:13;
then
((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) <= ((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))
by A213, XREAL_1:72;
then A214:
((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) <= 1
by A213, XCMPLX_1:60;
(qz `2) - (q1 `2) >= 0
by A212, XREAL_1:48;
hence
z in LSeg (
q1,
q2)
by A213, A214, A211;
verum
end; then
p1 in Q
by A4, A188, Th3;
hence
contradiction
by A104, A11, XBOOLE_0:def 4;
verum end; case A215:
p1 <> p2
;
contradictionA216:
1
<= len hb
by A91, XXREAL_0:2;
then
1
in dom hb
by FINSEQ_3:25;
then A217:
h2 /. 1
= g . (hb . 1)
by A142;
A218:
now not q1 = q2
0 in the
carrier of
I[01]
by BORSUK_1:43;
then
0 in dom g
by FUNCT_2:def 1;
then A219:
q1 in Q
by A4, A107, FUNCT_1:3;
0 in the
carrier of
I[01]
by BORSUK_1:43;
then A220:
0 in dom f
by FUNCT_2:def 1;
then A221:
p1 in P
by A3, A30, FUNCT_1:3;
assume A222:
q1 = q2
;
contradictionA223:
for
p being
Point of
(TOP-REAL 2) st
p in P holds
p `2 = q1 `2
A224:
now not p1 `1 = p2 `1 assume A225:
p1 `1 = p2 `1
;
contradiction
(
p1 `1 <= q1 `1 &
q1 `1 <= p2 `1 )
by A6, A219;
then A226:
q1 `1 = p1 `1
by A225, XXREAL_0:1;
p1 `2 = q1 `2
by A3, A30, A223, A220, FUNCT_1:3;
then
p1 = q1
by A226, TOPREAL3:6;
hence
contradiction
by A11, A221, A219, XBOOLE_0:def 4;
verum end; A227:
q1 in LSeg (
p1,
p2)
proof
1
in the
carrier of
I[01]
by BORSUK_1:43;
then
1
in dom f
by FUNCT_2:def 1;
then
f . 1
in rng f
by FUNCT_1:3;
then
(
q1 `2 <= p2 `2 &
p2 `2 <= q2 `2 )
by A3, A7, A71;
then A228:
q1 `2 = p2 `2
by A222, XXREAL_0:1;
set ln =
((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1));
A229:
(((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (p2 `1) =
(((q1 `1) - (p1 `1)) * (p2 `1)) / ((p2 `1) - (p1 `1))
by XCMPLX_1:74
.=
(((q1 `1) * (p2 `1)) - ((p1 `1) * (p2 `1))) / ((p2 `1) - (p1 `1))
;
A230:
(p2 `1) - (p1 `1) <> 0
by A224;
then 1
- (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) =
(((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))
by XCMPLX_1:60
.=
(((p2 `1) - (p1 `1)) - ((q1 `1) - (p1 `1))) / ((p2 `1) - (p1 `1))
by XCMPLX_1:120
.=
((p2 `1) - (q1 `1)) / ((p2 `1) - (p1 `1))
;
then A231:
(1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1) =
(((p2 `1) - (q1 `1)) * (p1 `1)) / ((p2 `1) - (p1 `1))
by XCMPLX_1:74
.=
(((p2 `1) * (p1 `1)) - ((q1 `1) * (p1 `1))) / ((p2 `1) - (p1 `1))
;
0 in the
carrier of
I[01]
by BORSUK_1:43;
then
0 in dom f
by FUNCT_2:def 1;
then
f . 0 in rng f
by FUNCT_1:3;
then
(
q1 `2 <= p1 `2 &
p1 `2 <= q2 `2 )
by A3, A7, A30;
then A232:
q1 `2 = p1 `2
by A222, XXREAL_0:1;
0 in the
carrier of
I[01]
by BORSUK_1:43;
then
0 in dom g
by FUNCT_2:def 1;
then A233:
g . 0 in rng g
by FUNCT_1:3;
then A234:
p1 `1 <= q1 `1
by A4, A6, A107;
A235:
(((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2)) `2 =
(((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) `2) + (((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `2)
by TOPREAL3:2
.=
((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `2)) + (((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `2)
by TOPREAL3:4
.=
((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (q1 `2)) + ((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (q1 `2))
by A232, A228, TOPREAL3:4
;
(((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2)) `1 =
(((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) `1) + (((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `1)
by TOPREAL3:2
.=
((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1)) + (((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `1)
by TOPREAL3:4
.=
((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1)) + ((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (p2 `1))
by TOPREAL3:4
.=
((((p2 `1) * (p1 `1)) - ((q1 `1) * (p1 `1))) + (((q1 `1) * (p2 `1)) - ((p1 `1) * (p2 `1)))) / ((p2 `1) - (p1 `1))
by A231, A229, XCMPLX_1:62
.=
((q1 `1) * ((p2 `1) - (p1 `1))) / ((p2 `1) - (p1 `1))
.=
(q1 `1) * (((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))
by XCMPLX_1:74
.=
(q1 `1) * 1
by A230, XCMPLX_1:60
;
then A236:
((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) = q1
by A235, TOPREAL3:6;
A237:
q1 `1 <= p2 `1
by A4, A6, A107, A233;
then
p2 `1 >= p1 `1
by A234, XXREAL_0:2;
then
p2 `1 > p1 `1
by A224, XXREAL_0:1;
then A238:
(p2 `1) - (p1 `1) > 0
by XREAL_1:50;
(q1 `1) - (p1 `1) <= (p2 `1) - (p1 `1)
by A237, XREAL_1:13;
then
((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) <= ((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))
by A238, XREAL_1:72;
then A239:
((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) <= 1
by A238, XCMPLX_1:60;
(q1 `1) - (p1 `1) >= 0
by A234, XREAL_1:48;
hence
q1 in LSeg (
p1,
p2)
by A238, A239, A236;
verum
end;
1
in the
carrier of
I[01]
by BORSUK_1:43;
then
1
in dom f
by FUNCT_2:def 1;
then A240:
p2 in P
by A3, A71, FUNCT_1:3;
P c= LSeg (
p1,
p2)
proof
(
q1 `2 <= p2 `2 &
p2 `2 <= q2 `2 )
by A7, A240;
then A241:
q1 `2 = p2 `2
by A222, XXREAL_0:1;
(
q1 `2 <= p1 `2 &
p1 `2 <= q2 `2 )
by A7, A221;
then A242:
q1 `2 = p1 `2
by A222, XXREAL_0:1;
let z be
object ;
TARSKI:def 3 ( not z in P or z in LSeg (p1,p2) )
assume A243:
z in P
;
z in LSeg (p1,p2)
then reconsider pz =
z as
Point of
(TOP-REAL 2) ;
A244:
pz `1 <= p2 `1
by A5, A243;
set ln =
((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1));
A245:
(((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (p2 `1) =
(((pz `1) - (p1 `1)) * (p2 `1)) / ((p2 `1) - (p1 `1))
by XCMPLX_1:74
.=
(((pz `1) * (p2 `1)) - ((p1 `1) * (p2 `1))) / ((p2 `1) - (p1 `1))
;
A246:
(p2 `1) - (p1 `1) <> 0
by A224;
then 1
- (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) =
(((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))
by XCMPLX_1:60
.=
(((p2 `1) - (p1 `1)) - ((pz `1) - (p1 `1))) / ((p2 `1) - (p1 `1))
by XCMPLX_1:120
.=
((p2 `1) - (pz `1)) / ((p2 `1) - (p1 `1))
;
then A247:
(1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1) =
(((p2 `1) - (pz `1)) * (p1 `1)) / ((p2 `1) - (p1 `1))
by XCMPLX_1:74
.=
(((p2 `1) * (p1 `1)) - ((pz `1) * (p1 `1))) / ((p2 `1) - (p1 `1))
;
A248:
(((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2)) `1 =
(((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) `1) + (((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `1)
by TOPREAL3:2
.=
((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1)) + (((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `1)
by TOPREAL3:4
.=
((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1)) + ((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (p2 `1))
by TOPREAL3:4
.=
((((p2 `1) * (p1 `1)) - ((pz `1) * (p1 `1))) + (((pz `1) * (p2 `1)) - ((p1 `1) * (p2 `1)))) / ((p2 `1) - (p1 `1))
by A247, A245, XCMPLX_1:62
.=
((pz `1) * ((p2 `1) - (p1 `1))) / ((p2 `1) - (p1 `1))
.=
(pz `1) * (((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))
by XCMPLX_1:74
.=
(pz `1) * 1
by A246, XCMPLX_1:60
.=
pz `1
;
A249:
(
q1 `2 <= pz `2 &
pz `2 <= q2 `2 )
by A7, A243;
(((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2)) `2 =
(((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) `2) + (((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `2)
by TOPREAL3:2
.=
((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `2)) + (((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `2)
by TOPREAL3:4
.=
((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (q1 `2)) + ((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (q1 `2))
by A242, A241, TOPREAL3:4
.=
pz `2
by A222, A249, XXREAL_0:1
;
then A250:
((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) = pz
by A248, TOPREAL3:6;
A251:
p1 `1 <= pz `1
by A5, A243;
then
p2 `1 >= p1 `1
by A244, XXREAL_0:2;
then
p2 `1 > p1 `1
by A224, XXREAL_0:1;
then A252:
(p2 `1) - (p1 `1) > 0
by XREAL_1:50;
(pz `1) - (p1 `1) <= (p2 `1) - (p1 `1)
by A244, XREAL_1:13;
then
((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) <= ((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))
by A252, XREAL_1:72;
then A253:
((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) <= 1
by A252, XCMPLX_1:60;
(pz `1) - (p1 `1) >= 0
by A251, XREAL_1:48;
hence
z in LSeg (
p1,
p2)
by A252, A253, A250;
verum
end; then
q1 in P
by A3, A227, Th3;
hence
contradiction
by A171, A11, XBOOLE_0:def 4;
verum end;
len hb in dom hb
by A216, FINSEQ_3:25;
then A254:
g2 . 1
<> g2 . (len g2)
by A107, A149, A89, A90, A95, A142, A157, A158, A166, A106, A218, A217;
f2 /. 1
<> f2 /. (len f2)
by A30, A71, A14, A15, A20, A21, A81, A82, A29, A172, A88, A102, A23, A215;
then
L~ f2 meets L~ g2
by A80, A84, A156, A160, A172, A88, A178, A169, A174, A175, A179, A168, A173, A176, A170, A177, A254, JGRAPH_1:26;
then consider s being
object such that A255:
s in L~ f2
and A256:
s in L~ g2
by XBOOLE_0:3;
reconsider ps =
s as
Point of
(TOP-REAL 2) by A255;
ps in union { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) }
by A255, TOPREAL1:def 4;
then consider x being
set such that A257:
(
ps in x &
x in { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } )
by TARSKI:def 4;
ps in union { (LSeg (g2,j)) where j is Nat : ( 1 <= j & j + 1 <= len g2 ) }
by A256, TOPREAL1:def 4;
then consider y being
set such that A258:
(
ps in y &
y in { (LSeg (g2,j)) where j is Nat : ( 1 <= j & j + 1 <= len g2 ) } )
by TARSKI:def 4;
consider i being
Nat such that A259:
x = LSeg (
f2,
i)
and A260:
1
<= i
and A261:
i + 1
<= len f2
by A257;
LSeg (
f2,
i)
= LSeg (
(f2 /. i),
(f2 /. (i + 1)))
by A260, A261, TOPREAL1:def 3;
then A262:
|.(ps - (f2 /. i)).| <= |.((f2 /. i) - (f2 /. (i + 1))).|
by A257, A259, JGRAPH_1:36;
i < len f2
by A261, NAT_1:13;
then
i in dom f2
by A260, FINSEQ_3:25;
then consider k being
Nat such that A263:
k in dom h1
and A264:
|.((f2 /. i) - (h1 /. k)).| < (min_dist_min (P9,Q9)) / 5
by A85;
consider j being
Nat such that A265:
y = LSeg (
g2,
j)
and A266:
1
<= j
and A267:
j + 1
<= len g2
by A258;
LSeg (
g2,
j)
= LSeg (
(g2 /. j),
(g2 /. (j + 1)))
by A266, A267, TOPREAL1:def 3;
then A268:
|.(ps - (g2 /. j)).| <= |.((g2 /. j) - (g2 /. (j + 1))).|
by A258, A265, JGRAPH_1:36;
reconsider p11 =
h1 /. k as
Point of
(TOP-REAL 2) ;
|.((f2 /. i) - (f2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
by A86, A260, A261;
then
|.(ps - (f2 /. i)).| < (min_dist_min (P9,Q9)) / 5
by A262, XXREAL_0:2;
then
(
|.(ps - (h1 /. k)).| <= |.(ps - (f2 /. i)).| + |.((f2 /. i) - (h1 /. k)).| &
|.(ps - (f2 /. i)).| + |.((f2 /. i) - (h1 /. k)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) )
by A264, TOPRNS_1:34, XREAL_1:8;
then
|.(ps - (h1 /. k)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)
by XXREAL_0:2;
then A269:
|.(p11 - ps).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)
by TOPRNS_1:27;
A270:
k in Seg (len h1)
by A263, FINSEQ_1:def 3;
then
( 1
<= k &
k <= len h1 )
by FINSEQ_1:1;
then
h1 . k = h1 /. k
by FINSEQ_4:15;
then A271:
h1 /. k = f . (h . k)
by A21, A263;
j < len g2
by A267, NAT_1:13;
then
j in dom g2
by A266, FINSEQ_3:25;
then consider k9 being
Nat such that A272:
k9 in dom h2
and A273:
|.((g2 /. j) - (h2 /. k9)).| < (min_dist_min (P9,Q9)) / 5
by A161;
k9 in Seg (len h2)
by A272, FINSEQ_1:def 3;
then
k9 in dom hb
by A95, FINSEQ_1:def 3;
then A274:
(
hb . k9 in rng hb &
h2 /. k9 = g . (hb . k9) )
by A142, FUNCT_1:def 3;
reconsider q11 =
h2 /. k9 as
Point of
(TOP-REAL 2) ;
reconsider x1 =
p11,
x2 =
q11 as
Point of
(Euclid 2) by EUCLID:22;
dom g = the
carrier of
I[01]
by FUNCT_2:def 1;
then A275:
h2 /. k9 in rng g
by A92, A274, FUNCT_1:def 3;
k in dom h
by A20, A270, FINSEQ_1:def 3;
then A276:
h . k in rng h
by FUNCT_1:def 3;
dom f = the
carrier of
I[01]
by FUNCT_2:def 1;
then
h1 /. k in P
by A3, A17, A271, A276, FUNCT_1:def 3;
then
min_dist_min (
P9,
Q9)
<= dist (
x1,
x2)
by A4, A10, A9, A275, WEIERSTR:34;
then A277:
min_dist_min (
P9,
Q9)
<= |.(p11 - q11).|
by JGRAPH_1:28;
|.((g2 /. j) - (g2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5
by A162, A266, A267;
then
|.(ps - (g2 /. j)).| < (min_dist_min (P9,Q9)) / 5
by A268, XXREAL_0:2;
then
(
|.(ps - (h2 /. k9)).| <= |.(ps - (g2 /. j)).| + |.((g2 /. j) - (h2 /. k9)).| &
|.(ps - (g2 /. j)).| + |.((g2 /. j) - (h2 /. k9)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) )
by A273, TOPRNS_1:34, XREAL_1:8;
then
|.(ps - (h2 /. k9)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)
by XXREAL_0:2;
then
(
|.(p11 - q11).| <= |.(p11 - ps).| + |.(ps - q11).| &
|.(p11 - ps).| + |.(ps - q11).| < (((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)) + (((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)) )
by A269, TOPRNS_1:34, XREAL_1:8;
then
|.(p11 - q11).| < ((((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)) + ((min_dist_min (P9,Q9)) / 5)) + ((min_dist_min (P9,Q9)) / 5)
by XXREAL_0:2;
then
min_dist_min (
P9,
Q9)
< 4
* ((min_dist_min (P9,Q9)) / 5)
by A277, XXREAL_0:2;
then
(4 * ((min_dist_min (P9,Q9)) / 5)) - (5 * ((min_dist_min (P9,Q9)) / 5)) > 0
by XREAL_1:50;
then
((4 - 5) * ((min_dist_min (P9,Q9)) / 5)) / ((min_dist_min (P9,Q9)) / 5) > 0
by A13, XREAL_1:139;
then
4
- 5
> 0
by A12;
hence
contradiction
;
verum end;
hence
contradiction
; verum