let P, Q be non empty Subset of (TOP-REAL 2); for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & Q is_an_arc_of q1,q2 & ( 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); ( P is_an_arc_of p1,p2 & Q is_an_arc_of q1,q2 & ( 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
A1:
P is_an_arc_of p1,p2
and
A2:
Q is_an_arc_of q1,q2
and
A3:
for p being Point of (TOP-REAL 2) st p in P holds
( p1 `1 <= p `1 & p `1 <= p2 `1 )
and
A4:
for p being Point of (TOP-REAL 2) st p in Q holds
( p1 `1 <= p `1 & p `1 <= p2 `1 )
and
A5:
for p being Point of (TOP-REAL 2) st p in P holds
( q1 `2 <= p `2 & p `2 <= q2 `2 )
and
A6:
for p being Point of (TOP-REAL 2) st p in Q holds
( q1 `2 <= p `2 & p `2 <= q2 `2 )
; P meets Q
consider g being Function of I[01],((TOP-REAL 2) | Q) such that
A7:
g is being_homeomorphism
and
A8:
g . 0 = q1
and
A9:
g . 1 = q2
by A2, TOPREAL1:def 1;
A10:
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;
then reconsider P9 = P, Q9 = Q as Subset of (TopSpaceMetr (Euclid 2)) ;
P is compact
by A1, JORDAN5A:1;
then A11:
P9 is compact
by A10, COMPTS_1:23;
Q is compact
by A2, JORDAN5A:1;
then A12:
Q9 is compact
by A10, COMPTS_1:23;
set e = (min_dist_min (P9,Q9)) / 5;
consider f being Function of I[01],((TOP-REAL 2) | P) such that
A13:
f is being_homeomorphism
and
A14:
f . 0 = p1
and
A15:
f . 1 = p2
by A1, TOPREAL1:def 1;
consider f1 being Function of I[01],(TOP-REAL 2) such that
A16:
f = f1
and
A17:
f1 is continuous
and
f1 is one-to-one
by A13, JORDAN7:15;
consider g1 being Function of I[01],(TOP-REAL 2) such that
A18:
g = g1
and
A19:
g1 is continuous
and
g1 is one-to-one
by A7, JORDAN7:15;
assume
P /\ Q = {}
; XBOOLE_0:def 7 contradiction
then
P misses Q
;
then A20:
min_dist_min (P9,Q9) > 0
by A11, A12, Th37;
then A21:
(min_dist_min (P9,Q9)) / 5 > 0 / 5
by XREAL_1:74;
then consider hb being FinSequence of REAL such that
A22:
hb . 1 = 0
and
A23:
hb . (len hb) = 1
and
A24:
5 <= len hb
and
A25:
rng hb c= the carrier of I[01]
and
A26:
hb is increasing
and
A27:
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 = g1 .: R holds
diameter W < (min_dist_min (P9,Q9)) / 5
by A19, UNIFORM1:13;
consider h being FinSequence of REAL such that
A28:
h . 1 = 0
and
A29:
h . (len h) = 1
and
A30:
5 <= len h
and
A31:
rng h c= the carrier of I[01]
and
A32:
h is increasing
and
A33:
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 = f1 .: R holds
diameter W < (min_dist_min (P9,Q9)) / 5
by A17, A21, UNIFORM1:13;
deffunc H1( Nat) -> set = f1 . (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
A34:
len h19 = len h
and
A35:
for i being Nat st i in dom h19 holds
h19 . i = f1 . (h . i)
;
A36: dom g1 =
[#] I[01]
by A7, A18, TOPS_2:def 5
.=
the carrier of I[01]
;
rng h19 c= the carrier of (TOP-REAL 2)
proof
let y be
object ;
TARSKI:def 3 ( not y in rng h19 or y in the carrier of (TOP-REAL 2) )
assume
y in rng h19
;
y in the carrier of (TOP-REAL 2)
then consider x being
object such that A37:
x in dom h19
and A38:
y = h19 . x
by FUNCT_1:def 3;
reconsider i =
x as
Element of
NAT by A37;
dom h19 = Seg (len h19)
by FINSEQ_1:def 3;
then
i in dom h
by A34, A37, FINSEQ_1:def 3;
then A39:
h . i in rng h
by FUNCT_1:def 3;
A40:
dom f1 =
[#] I[01]
by A13, A16, TOPS_2:def 5
.=
the
carrier of
I[01]
;
A41:
rng f =
[#] ((TOP-REAL 2) | P)
by A13, TOPS_2:def 5
.=
P
by PRE_TOPC:def 5
;
h19 . i = f1 . (h . i)
by A35, A37;
then
h19 . i in rng f
by A16, A31, A39, A40, FUNCT_1:def 3;
hence
y in the
carrier of
(TOP-REAL 2)
by A38, A41;
verum
end;
then reconsider h1 = h19 as FinSequence of (TOP-REAL 2) by FINSEQ_1:def 4;
A42:
len h1 >= 1
by A30, A34, XXREAL_0:2;
then A43:
h1 . 1 = h1 /. 1
by FINSEQ_4:15;
A44:
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) ;
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 A45:
1
<= i
and A46:
i + 1
<= len h1
;
|.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
A47:
1
< i + 1
by A45, NAT_1:13;
then A48:
h . (i + 1) = h /. (i + 1)
by A34, A46, FINSEQ_4:15;
A49:
i + 1
in dom h19
by A46, A47, FINSEQ_3:25;
then A50:
h19 . (i + 1) = f1 . (h . (i + 1))
by A35;
then A51:
h1 /. (i + 1) = f1 . (h . (i + 1))
by A46, A47, FINSEQ_4:15;
A52:
i < len h1
by A46, NAT_1:13;
then A53:
h . i = h /. i
by A34, A45, FINSEQ_4:15;
A54:
i in dom h
by A34, A45, A52, FINSEQ_3:25;
then A55:
h . i in rng h
by FUNCT_1:def 3;
A56:
i + 1
in dom h
by A34, A46, A47, 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 A31, A55, A53, A48, BORSUK_1:40, XXREAL_2:def 12;
reconsider W =
f1 .: R as
Subset of
(Euclid 2) by TOPREAL3:8;
A57:
Pa is
compact
by A1, JORDAN5A:1;
reconsider Pa =
Pa as non
empty Subset of
(TOP-REAL 2) ;
A58:
rng f =
[#] ((TOP-REAL 2) | P)
by A13, TOPS_2:def 5
.=
P
by PRE_TOPC:def 5
;
set r1 =
(((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1;
A59:
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 A60:
x in W1
and A61:
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 A60, A61;
A62:
(
S-bound Pa <= pw2 `2 &
pw2 `2 <= N-bound Pa )
by A57, A61, PSCOMP_1:24;
(
S-bound Pa <= pw1 `2 &
pw1 `2 <= N-bound Pa )
by A57, A60, PSCOMP_1:24;
then A63:
|.((pw1 `2) - (pw2 `2)).| <= (N-bound Pa) - (S-bound Pa)
by A62, Th27;
A64:
(
W-bound Pa <= pw2 `1 &
pw2 `1 <= E-bound Pa )
by A57, A61, PSCOMP_1:24;
(
W-bound Pa <= pw1 `1 &
pw1 `1 <= E-bound Pa )
by A57, A60, PSCOMP_1:24;
then
|.((pw1 `1) - (pw2 `1)).| <= (E-bound Pa) - (W-bound Pa)
by A64, Th27;
then A65:
|.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= ((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))
by A63, XREAL_1:7;
((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;
then A66:
|.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1
by A65, XXREAL_0:2;
(
dist (
x,
y)
= |.(pw1 - pw2).| &
|.(pw1 - pw2).| <= |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| )
by Th28, Th32;
hence
dist (
x,
y)
<= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1
by A66, XXREAL_0:2;
verum
end;
A67:
p1 in Pa
by A1, TOPREAL1:1;
then
(
S-bound Pa <= p1 `2 &
p1 `2 <= N-bound Pa )
by A57, PSCOMP_1:24;
then
S-bound Pa <= N-bound Pa
by XXREAL_0:2;
then A68:
0 <= (N-bound Pa) - (S-bound Pa)
by XREAL_1:48;
(
W-bound Pa <= p1 `1 &
p1 `1 <= E-bound Pa )
by A57, A67, 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 A69:
W1 is
bounded
by A68, A59, TBSP_1:def 7;
A70:
dom f1 =
[#] I[01]
by A13, A16, TOPS_2:def 5
.=
the
carrier of
I[01]
;
i + 1
in dom h
by A34, A46, A47, FINSEQ_3:25;
then
h . (i + 1) in rng h
by FUNCT_1:def 3;
then
h19 . (i + 1) in rng f
by A16, A31, A50, A70, FUNCT_1:def 3;
then A71:
f1 . (h . (i + 1)) is
Element of
(TOP-REAL 2)
by A35, A49, A58;
A72:
i in dom h19
by A45, A52, FINSEQ_3:25;
then A73:
h19 . i = f1 . (h . i)
by A35;
then
h19 . i in rng f
by A16, A31, A55, A70, FUNCT_1:def 3;
then
f1 . (h . i) is
Element of
(TOP-REAL 2)
by A35, A72, A58;
then reconsider w1 =
f1 . (h . i),
w2 =
f1 . (h . (i + 1)) as
Point of
(Euclid 2) by A71, TOPREAL3:8;
i < i + 1
by NAT_1:13;
then A74:
h /. i <= h /. (i + 1)
by A32, A54, A53, A56, A48, SEQM_3:def 1;
then
h . i in R
by A53, XXREAL_1:1;
then A75:
w1 in f1 .: R
by A70, FUNCT_1:def 6;
h . (i + 1) in R
by A48, A74, XXREAL_1:1;
then A76:
w2 in f1 .: R
by A70, FUNCT_1:def 6;
dom f1 = [#] I[01]
by A13, A16, TOPS_2:def 5;
then
P = f1 .: [.0,1.]
by A16, A58, BORSUK_1:40, RELAT_1:113;
then
W is
bounded
by A69, BORSUK_1:40, RELAT_1:123, TBSP_1:14;
then A77:
dist (
w1,
w2)
<= diameter W
by A75, A76, TBSP_1:def 8;
diameter W < (min_dist_min (P9,Q9)) / 5
by A33, A34, A45, A52;
then A78:
dist (
w1,
w2)
< (min_dist_min (P9,Q9)) / 5
by A77, XXREAL_0:2;
h1 /. i = f1 . (h . i)
by A45, A52, A73, FINSEQ_4:15;
hence
|.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
by A51, A78, Th28;
verum
end;
A79:
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 A34, A42, FINSEQ_3:25;
then
h1 . (len h1) = f1 . (h . (len h))
by A34, A35;
then A80:
h1 /. (len h1) = f1 . (h . (len h))
by A42, 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 A81:
i in dom h1
;
( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 )
then
h1 . i = f1 . (h . i)
by A35;
then A82:
h1 /. i = f1 . (h . i)
by A81, PARTFUN1:def 6;
i in Seg (len h)
by A34, A81, FINSEQ_1:def 3;
then
i in dom h
by FINSEQ_1:def 3;
then A83:
h . i in rng h
by FUNCT_1:def 3;
dom f1 =
[#] I[01]
by A13, A16, TOPS_2:def 5
.=
the
carrier of
I[01]
;
then A84:
h1 /. i in rng f
by A16, A31, A82, A83, FUNCT_1:def 3;
1
in dom h19
by A42, FINSEQ_3:25;
then
h1 . 1
= f1 . (h . 1)
by A35;
then A85:
h1 /. 1
= f1 . (h . 1)
by A42, FINSEQ_4:15;
rng f =
[#] ((TOP-REAL 2) | P)
by A13, TOPS_2:def 5
.=
P
by PRE_TOPC:def 5
;
hence
(
(h1 /. 1) `1 <= (h1 /. i) `1 &
(h1 /. i) `1 <= (h1 /. (len h1)) `1 )
by A3, A14, A15, A16, A28, A29, A85, A80, A84;
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 A88:
X_axis h1 lies_between (X_axis h1) . 1,(X_axis h1) . (len h1)
by GOBOARD4:def 2;
A89:
for i being Nat st i in dom h1 holds
( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 )
proof
let i be
Nat;
( i in dom h1 implies ( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 ) )
A90:
rng f =
[#] ((TOP-REAL 2) | P)
by A13, TOPS_2:def 5
.=
P
by PRE_TOPC:def 5
;
assume A91:
i in dom h1
;
( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 )
then
h1 . i = f1 . (h . i)
by A35;
then A92:
h1 /. i = f1 . (h . i)
by A91, PARTFUN1:def 6;
i in Seg (len h1)
by A91, FINSEQ_1:def 3;
then
i in dom h
by A34, FINSEQ_1:def 3;
then A93:
h . i in rng h
by FUNCT_1:def 3;
dom f1 =
[#] I[01]
by A13, A16, TOPS_2:def 5
.=
the
carrier of
I[01]
;
then
h1 /. i in rng f
by A16, A31, A92, A93, FUNCT_1:def 3;
hence
(
q1 `2 <= (h1 /. i) `2 &
(h1 /. i) `2 <= q2 `2 )
by A5, A90;
verum
end;
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
Y_axis h1 lies_between q1 `2 ,q2 `2
by GOBOARD4:def 2;
then consider f2 being FinSequence of (TOP-REAL 2) such that
A95:
f2 is special
and
A96:
f2 . 1 = h1 . 1
and
A97:
f2 . (len f2) = h1 . (len h1)
and
A98:
len f2 >= len h1
and
A99:
( X_axis f2 lies_between (X_axis h1) . 1,(X_axis h1) . (len h1) & Y_axis f2 lies_between q1 `2 ,q2 `2 )
and
A100:
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
A101:
for j being Nat st 1 <= j & j + 1 <= len f2 holds
|.((f2 /. j) - (f2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5
by A21, A44, A42, A88, Th38;
A102:
len f2 >= 1
by A42, A98, XXREAL_0:2;
then A103:
f2 . (len f2) = f2 /. (len f2)
by FINSEQ_4:15;
deffunc H2( Nat) -> set = g1 . (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
A104:
len h29 = len hb
and
A105:
for i being Nat st i in dom h29 holds
h29 . i = g1 . (hb . i)
;
rng h29 c= the carrier of (TOP-REAL 2)
proof
let y be
object ;
TARSKI:def 3 ( not y in rng h29 or y in the carrier of (TOP-REAL 2) )
assume
y in rng h29
;
y in the carrier of (TOP-REAL 2)
then consider x being
object such that A106:
x in dom h29
and A107:
y = h29 . x
by FUNCT_1:def 3;
reconsider i =
x as
Element of
NAT by A106;
dom h29 = Seg (len h29)
by FINSEQ_1:def 3;
then
i in dom hb
by A104, A106, FINSEQ_1:def 3;
then A108:
hb . i in rng hb
by FUNCT_1:def 3;
A109:
dom g1 =
[#] I[01]
by A7, A18, TOPS_2:def 5
.=
the
carrier of
I[01]
;
A110:
rng g =
[#] ((TOP-REAL 2) | Q)
by A7, TOPS_2:def 5
.=
Q
by PRE_TOPC:def 5
;
h29 . i = g1 . (hb . i)
by A105, A106;
then
h29 . i in rng g
by A18, A25, A108, A109, FUNCT_1:def 3;
hence
y in the
carrier of
(TOP-REAL 2)
by A107, A110;
verum
end;
then reconsider h2 = h29 as FinSequence of (TOP-REAL 2) by FINSEQ_1:def 4;
A111: rng f =
[#] ((TOP-REAL 2) | P)
by A13, TOPS_2:def 5
.=
P
by PRE_TOPC:def 5
;
A112:
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) ;
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 A113:
1
<= i
and A114:
i + 1
<= len h2
;
|.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
A115:
Qa is
compact
by A2, JORDAN5A:1;
reconsider Qa =
Qa as non
empty Subset of
(TOP-REAL 2) ;
A116:
rng g =
[#] ((TOP-REAL 2) | Q)
by A7, TOPS_2:def 5
.=
Q
by PRE_TOPC:def 5
;
set r1 =
(((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1;
A117:
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 A118:
x in W1
and A119:
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 A118, A119;
A120:
(
S-bound Qa <= pw2 `2 &
pw2 `2 <= N-bound Qa )
by A115, A119, PSCOMP_1:24;
(
S-bound Qa <= pw1 `2 &
pw1 `2 <= N-bound Qa )
by A115, A118, PSCOMP_1:24;
then A121:
|.((pw1 `2) - (pw2 `2)).| <= (N-bound Qa) - (S-bound Qa)
by A120, Th27;
A122:
(
W-bound Qa <= pw2 `1 &
pw2 `1 <= E-bound Qa )
by A115, A119, PSCOMP_1:24;
(
W-bound Qa <= pw1 `1 &
pw1 `1 <= E-bound Qa )
by A115, A118, PSCOMP_1:24;
then
|.((pw1 `1) - (pw2 `1)).| <= (E-bound Qa) - (W-bound Qa)
by A122, Th27;
then A123:
|.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= ((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))
by A121, XREAL_1:7;
((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;
then A124:
|.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1
by A123, XXREAL_0:2;
(
dist (
x,
y)
= |.(pw1 - pw2).| &
|.(pw1 - pw2).| <= |.((pw1 `1) - (pw2 `1)).| + |.((pw1 `2) - (pw2 `2)).| )
by Th28, Th32;
hence
dist (
x,
y)
<= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1
by A124, XXREAL_0:2;
verum
end;
A125:
q1 in Qa
by A2, TOPREAL1:1;
then
(
S-bound Qa <= q1 `2 &
q1 `2 <= N-bound Qa )
by A115, PSCOMP_1:24;
then
S-bound Qa <= N-bound Qa
by XXREAL_0:2;
then A126:
0 <= (N-bound Qa) - (S-bound Qa)
by XREAL_1:48;
(
W-bound Qa <= q1 `1 &
q1 `1 <= E-bound Qa )
by A115, A125, 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 A127:
W1 is
bounded
by A126, A117, TBSP_1:def 7;
A128:
dom g1 =
[#] I[01]
by A7, A18, TOPS_2:def 5
.=
the
carrier of
I[01]
;
A129:
1
< i + 1
by A113, NAT_1:13;
then
i + 1
in Seg (len hb)
by A104, A114, FINSEQ_1:1;
then
i + 1
in dom hb
by FINSEQ_1:def 3;
then A130:
hb . (i + 1) in rng hb
by FUNCT_1:def 3;
A131:
i < len h2
by A114, NAT_1:13;
then A132:
hb . i = hb /. i
by A104, A113, FINSEQ_4:15;
A133:
i + 1
in dom h29
by A114, A129, FINSEQ_3:25;
then
h29 . (i + 1) = g1 . (hb . (i + 1))
by A105;
then
h29 . (i + 1) in rng g
by A18, A25, A128, A130, FUNCT_1:def 3;
then A134:
g1 . (hb . (i + 1)) is
Element of
(TOP-REAL 2)
by A105, A133, A116;
A135:
hb . (i + 1) = hb /. (i + 1)
by A104, A114, A129, FINSEQ_4:15;
i in dom h29
by A113, A131, FINSEQ_3:25;
then A136:
h29 . i = g1 . (hb . i)
by A105;
i in Seg (len hb)
by A104, A113, A131, FINSEQ_1:1;
then A137:
i in dom hb
by FINSEQ_1:def 3;
then A138:
hb . i in rng hb
by FUNCT_1:def 3;
then
h29 . i in rng g
by A18, A25, A136, A128, FUNCT_1:def 3;
then reconsider w1 =
g1 . (hb . i),
w2 =
g1 . (hb . (i + 1)) as
Point of
(Euclid 2) by A136, A116, A134, TOPREAL3:8;
i + 1
in Seg (len hb)
by A104, A114, A129, FINSEQ_1:1;
then A139:
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 A25, A138, A132, A135, BORSUK_1:40, XXREAL_2:def 12;
i < i + 1
by NAT_1:13;
then A140:
hb /. i <= hb /. (i + 1)
by A26, A137, A132, A139, A135, SEQM_3:def 1;
then
hb . i in R
by A132, XXREAL_1:1;
then A141:
w1 in g1 .: R
by A128, FUNCT_1:def 6;
hb . (i + 1) in R
by A135, A140, XXREAL_1:1;
then A142:
w2 in g1 .: R
by A128, FUNCT_1:def 6;
reconsider W =
g1 .: R as
Subset of
(Euclid 2) by TOPREAL3:8;
dom g1 = [#] I[01]
by A7, A18, TOPS_2:def 5;
then
Q = g1 .: [.0,1.]
by A18, A116, BORSUK_1:40, RELAT_1:113;
then
W is
bounded
by A127, BORSUK_1:40, RELAT_1:123, TBSP_1:14;
then A143:
dist (
w1,
w2)
<= diameter W
by A141, A142, TBSP_1:def 8;
diameter W < (min_dist_min (P9,Q9)) / 5
by A27, A104, A113, A131;
then A144:
dist (
w1,
w2)
< (min_dist_min (P9,Q9)) / 5
by A143, XXREAL_0:2;
h2 . (i + 1) = h2 /. (i + 1)
by A114, A129, FINSEQ_4:15;
then A145:
h2 /. (i + 1) = g1 . (hb . (i + 1))
by A105, A133;
h2 /. i = g1 . (hb . i)
by A113, A131, A136, FINSEQ_4:15;
hence
|.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
by A145, A144, Th28;
verum
end;
A146:
1 <= len hb
by A24, XXREAL_0:2;
then A147:
len hb in dom hb
by FINSEQ_3:25;
A148:
1 <= len hb
by A24, XXREAL_0:2;
then A149:
h2 . (len h2) = h2 /. (len h2)
by A104, FINSEQ_4:15;
A150:
dom hb = Seg (len hb)
by FINSEQ_1:def 3;
A151:
for i being Nat st i in dom hb holds
h2 /. i = g1 . (hb . i)
A154:
f2 . 1 = f2 /. 1
by A102, FINSEQ_4:15;
A155:
1 <= len h
by A30, XXREAL_0:2;
then
1 in dom h19
by A34, FINSEQ_3:25;
then A156:
h1 /. 1 = f1 . (h . 1)
by A35, A43;
len h in dom h19
by A34, A155, FINSEQ_3:25;
then A157:
f2 /. 1 <> f2 /. (len f2)
by A1, A14, A15, A16, A28, A29, A34, A35, A96, A97, A43, A154, A103, A156, JORDAN6:37;
5 <= len f2
by A30, A34, A98, XXREAL_0:2;
then A158:
2 <= len f2
by XXREAL_0:2;
A159:
h1 . (len h1) = h1 /. (len h1)
by A42, FINSEQ_4:15;
then A160: (X_axis f2) . (len f2) =
(h1 /. (len h1)) `1
by A97, A102, A103, Th40
.=
(X_axis h1) . (len h1)
by A42, Th40
;
A161:
h2 . 1 = h2 /. 1
by A148, A104, FINSEQ_4:15;
A162:
len h2 >= 1
by A24, A104, XXREAL_0:2;
A163:
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 A104, FINSEQ_1:def 3;
then A164:
(
h2 /. i = g1 . (hb . i) &
hb . i in rng hb )
by A151, FUNCT_1:def 3;
dom g1 =
[#] I[01]
by A7, A18, TOPS_2:def 5
.=
the
carrier of
I[01]
;
then A165:
h2 /. i in rng g
by A18, A25, A164, FUNCT_1:def 3;
1
in Seg (len hb)
by A104, A162, FINSEQ_1:1;
then
1
in dom hb
by FINSEQ_1:def 3;
then A166:
h2 /. 1
= g1 . (hb . 1)
by A151;
len hb in Seg (len hb)
by A104, A162, FINSEQ_1:1;
then
len hb in dom hb
by FINSEQ_1:def 3;
then A167:
h2 /. (len h2) = g1 . (hb . (len hb))
by A104, A151;
rng g =
[#] ((TOP-REAL 2) | Q)
by A7, TOPS_2:def 5
.=
Q
by PRE_TOPC:def 5
;
hence
(
(h2 /. 1) `2 <= (h2 /. i) `2 &
(h2 /. i) `2 <= (h2 /. (len h2)) `2 )
by A6, A8, A9, A18, A22, A23, A166, A167, A165;
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 A170:
Y_axis h2 lies_between (Y_axis h2) . 1,(Y_axis h2) . (len h2)
by GOBOARD4:def 2;
A171:
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
X_axis h2 lies_between p1 `1 ,p2 `1
by GOBOARD4:def 2;
then consider g2 being FinSequence of (TOP-REAL 2) such that
A175:
g2 is special
and
A176:
g2 . 1 = h2 . 1
and
A177:
g2 . (len g2) = h2 . (len h2)
and
A178:
len g2 >= len h2
and
A179:
( Y_axis g2 lies_between (Y_axis h2) . 1,(Y_axis h2) . (len h2) & X_axis g2 lies_between p1 `1 ,p2 `1 )
and
A180:
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
A181:
for j being Nat st 1 <= j & j + 1 <= len g2 holds
|.((g2 /. j) - (g2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5
by A21, A162, A170, A112, Th39;
5 <= len g2
by A24, A104, A178, XXREAL_0:2;
then A182:
2 <= len g2
by XXREAL_0:2;
A183:
len g2 >= 1
by A162, A178, XXREAL_0:2;
then
g2 . 1 = g2 /. 1
by FINSEQ_4:15;
then A184: (Y_axis g2) . 1 =
(h2 /. 1) `2
by A176, A183, A161, Th41
.=
(Y_axis h2) . 1
by A162, Th41
;
1 in dom hb
by A146, FINSEQ_3:25;
then
h2 /. 1 = g1 . (hb . 1)
by A151;
then A185:
g2 . 1 <> g2 . (len g2)
by A2, A8, A9, A18, A22, A23, A104, A151, A176, A177, A161, A149, A147, JORDAN6:37;
len hb in dom hb
by A148, FINSEQ_3:25;
then A186:
g2 . (len g2) = q2
by A9, A18, A23, A104, A151, A177, A149;
g2 /. (len g2) = g2 . (len g2)
by A183, FINSEQ_4:15;
then A187:
(Y_axis g2) . (len g2) = q2 `2
by A183, A186, Th41;
1 in dom hb
by A148, FINSEQ_3:25;
then A188:
h2 /. 1 = q1
by A8, A18, A22, A151;
A189: rng g =
[#] ((TOP-REAL 2) | Q)
by A7, TOPS_2:def 5
.=
Q
by PRE_TOPC:def 5
;
len h in dom h19
by A34, A42, FINSEQ_3:25;
then
h1 /. (len h1) = p2
by A15, A16, A29, A34, A35, A159;
then A190:
(X_axis f2) . (len f2) = p2 `1
by A97, A102, A159, A103, Th40;
1 in dom h19
by A42, FINSEQ_3:25;
then
h1 . 1 = f1 . (h . 1)
by A35;
then A191:
(X_axis f2) . 1 = p1 `1
by A14, A16, A28, A96, A102, A154, Th40;
g2 . (len g2) = g2 /. (len g2)
by A183, FINSEQ_4:15;
then A192: (Y_axis g2) . (len g2) =
(h2 /. (len h2)) `2
by A177, A183, A149, Th41
.=
(Y_axis h2) . (len h2)
by A162, Th41
;
g2 /. 1 = g2 . 1
by A183, FINSEQ_4:15;
then A193:
(Y_axis g2) . 1 = q1 `2
by A176, A183, A188, A161, Th41;
(X_axis f2) . 1 =
(h1 /. 1) `1
by A96, A102, A43, A154, Th40
.=
(X_axis h1) . 1
by A42, Th40
;
then
L~ f2 meets L~ g2
by A95, A99, A175, A179, A154, A103, A191, A190, A193, A187, A160, A184, A192, A158, A182, A157, A185, Th26;
then consider s being object such that
A194:
s in L~ f2
and
A195:
s in L~ g2
by XBOOLE_0:3;
reconsider ps = s as Point of (TOP-REAL 2) by A194;
ps in union { (LSeg (g2,j)) where j is Nat : ( 1 <= j & j + 1 <= len g2 ) }
by A195, TOPREAL1:def 4;
then consider y being set such that
A196:
( ps in y & y in { (LSeg (g2,j)) where j is Nat : ( 1 <= j & j + 1 <= len g2 ) } )
by TARSKI:def 4;
ps in union { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) }
by A194, TOPREAL1:def 4;
then consider x being set such that
A197:
( ps in x & x in { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } )
by TARSKI:def 4;
consider i being Nat such that
A198:
x = LSeg (f2,i)
and
A199:
1 <= i
and
A200:
i + 1 <= len f2
by A197;
LSeg (f2,i) = LSeg ((f2 /. i),(f2 /. (i + 1)))
by A199, A200, TOPREAL1:def 3;
then A201:
|.(ps - (f2 /. i)).| <= |.((f2 /. i) - (f2 /. (i + 1))).|
by A197, A198, Th35;
i < len f2
by A200, NAT_1:13;
then
i in dom f2
by A199, FINSEQ_3:25;
then consider k being Nat such that
A202:
k in dom h1
and
A203:
|.((f2 /. i) - (h1 /. k)).| < (min_dist_min (P9,Q9)) / 5
by A100;
k in dom h
by A34, A202, FINSEQ_3:29;
then A204:
h . k in rng h
by FUNCT_1:def 3;
reconsider p11 = h1 /. k as Point of (TOP-REAL 2) ;
|.((f2 /. i) - (f2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
by A101, A199, A200;
then
|.(ps - (f2 /. i)).| < (min_dist_min (P9,Q9)) / 5
by A201, 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 A203, 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 A205:
|.(p11 - ps).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)
by TOPRNS_1:27;
k in Seg (len h1)
by A202, FINSEQ_1:def 3;
then
( 1 <= k & k <= len h1 )
by FINSEQ_1:1;
then
h1 . k = h1 /. k
by FINSEQ_4:15;
then A206:
h1 /. k = f1 . (h . k)
by A35, A202;
consider j being Nat such that
A207:
y = LSeg (g2,j)
and
A208:
1 <= j
and
A209:
j + 1 <= len g2
by A196;
LSeg (g2,j) = LSeg ((g2 /. j),(g2 /. (j + 1)))
by A208, A209, TOPREAL1:def 3;
then A210:
|.(ps - (g2 /. j)).| <= |.((g2 /. j) - (g2 /. (j + 1))).|
by A196, A207, Th35;
j < len g2
by A209, NAT_1:13;
then
j in Seg (len g2)
by A208, FINSEQ_1:1;
then
j in dom g2
by FINSEQ_1:def 3;
then consider k9 being Nat such that
A211:
k9 in dom h2
and
A212:
|.((g2 /. j) - (h2 /. k9)).| < (min_dist_min (P9,Q9)) / 5
by A180;
k9 in Seg (len h2)
by A211, FINSEQ_1:def 3;
then A213:
k9 in dom hb
by A104, FINSEQ_1:def 3;
then A214:
hb . k9 in rng hb
by FUNCT_1:def 3;
reconsider q11 = h2 /. k9 as Point of (TOP-REAL 2) ;
|.((g2 /. j) - (g2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5
by A181, A208, A209;
then
|.(ps - (g2 /. j)).| < (min_dist_min (P9,Q9)) / 5
by A210, 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 A212, 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 A205, TOPRNS_1:34, XREAL_1:8;
then A215:
|.(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;
h2 /. k9 = g1 . (hb . k9)
by A151, A213;
then A216:
h2 /. k9 in rng g
by A18, A25, A214, A36, FUNCT_1:def 3;
reconsider x1 = p11, x2 = q11 as Point of (Euclid 2) by EUCLID:22;
dom f1 =
[#] I[01]
by A13, A16, TOPS_2:def 5
.=
the carrier of I[01]
;
then
h1 /. k in P
by A16, A31, A206, A204, A111, FUNCT_1:def 3;
then
min_dist_min (P9,Q9) <= dist (x1,x2)
by A11, A12, A216, A189, WEIERSTR:34;
then
min_dist_min (P9,Q9) <= |.(p11 - q11).|
by Th28;
then
min_dist_min (P9,Q9) < 4 * ((min_dist_min (P9,Q9)) / 5)
by A215, 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 A21, XREAL_1:139;
then
4 - 5 > 0
by A20;
hence
contradiction
; verum