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