let P, Q be non empty Subset of (TOP-REAL 2); :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: ( 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
A1:
rng f = P
and
A2:
rng g = Q
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 )
; :: thesis: P meets Q
A7:
( f . 0 = p1 & f . 1 = p2 )
by BORSUK_2:def 4;
A8:
( g . 0 = q1 & g . 1 = q2 )
by BORSUK_2:def 4;
reconsider P' = P, Q' = Q as Subset of (TopSpaceMetr (Euclid 2)) ;
A9:
[#] I[01] is compact
by COMPTS_1:10;
A10:
f .: the carrier of I[01] = rng f
by FUNCT_2:45;
A11:
g .: ([#] I[01] ) = rng g
by FUNCT_2:45;
A12:
0 in the carrier of I[01]
by BORSUK_1:86;
then
0 in dom f
by FUNCT_2:def 1;
then A13:
p1 in P'
by A1, A7, FUNCT_1:def 5;
0 in dom g
by A12, FUNCT_2:def 1;
then A14:
q1 in Q'
by A2, A8, FUNCT_1:def 5;
A15:
( P' <> {} & P' is compact & Q' <> {} & Q' is compact )
by A1, A2, A9, A10, A11, WEIERSTR:14;
assume A16:
P /\ Q = {}
; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then
P misses Q
by XBOOLE_0:def 7;
then A17:
min_dist_min P',Q' > 0
by A15, JGRAPH_1:55;
set e = (min_dist_min P',Q') / 5;
A18:
(min_dist_min P',Q') / 5 > 0 / 5
by A17, XREAL_1:76;
then consider h being FinSequence of REAL such that
A19:
( 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 = f .: R holds
diameter W < (min_dist_min P',Q') / 5 ) )
by Th1;
deffunc H1( Nat) -> set = f . (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
A20:
( len h1' = len h & ( for i being Nat st i in dom h1' holds
h1' . i = f . (h . i) ) )
;
rng h1' c= the carrier of (TOP-REAL 2)
then reconsider h1 = h1' as FinSequence of (TOP-REAL 2) by FINSEQ_1:def 4;
A25:
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 A26:
( 1
<= i &
i + 1
<= len h1 )
;
:: thesis: |.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min P',Q') / 5
then A27:
i < len h1
by NAT_1:13;
A28:
1
< i + 1
by A26, NAT_1:13;
then A29:
i + 1
in dom h1'
by A26, FINSEQ_3:27;
A30:
i in dom h1'
by A26, A27, FINSEQ_3:27;
then A31:
h1' . i = f . (h . i)
by A20;
then A32:
h1 /. i = f . (h . i)
by A26, A27, FINSEQ_4:24;
A33:
h1' . (i + 1) = f . (h . (i + 1))
by A20, A29;
then A34:
h1 /. (i + 1) = f . (h . (i + 1))
by A26, A28, FINSEQ_4:24;
A35:
i in dom h
by A20, A26, A27, FINSEQ_3:27;
then A36:
h . i in rng h
by FUNCT_1:def 5;
A37:
dom f = the
carrier of
I[01]
by FUNCT_2:def 1;
then
h1' . i in rng f
by A19, A31, A36, FUNCT_1:def 5;
then A38:
f . (h . i) is
Element of
(TOP-REAL 2)
by A20, A30;
i + 1
in dom h
by A20, A26, A28, FINSEQ_3:27;
then
h . (i + 1) in rng h
by FUNCT_1:def 5;
then
h1' . (i + 1) in rng f
by A19, A33, A37, FUNCT_1:def 5;
then A39:
f . (h . (i + 1)) is
Element of
(TOP-REAL 2)
by A20, A29;
A40:
h . i = h /. i
by A20, A26, A27, FINSEQ_4:24;
A41:
i + 1
in dom h
by A20, A26, A28, FINSEQ_3:27;
then A42:
h . (i + 1) in rng h
by FUNCT_1:def 5;
A43:
h . (i + 1) = h /. (i + 1)
by A20, A26, A28, FINSEQ_4:24;
i < i + 1
by NAT_1:13;
then A44:
(
0 <= h /. i &
h /. i <= h /. (i + 1) &
h /. (i + 1) <= 1 )
by A19, A35, A36, A40, A41, A42, A43, 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) ;
A45:
[#] I[01] is
compact
by COMPTS_1:10;
f .: the
carrier of
I[01] = rng f
by FUNCT_2:45;
then A46:
Pa is
compact
by A1, A45, WEIERSTR:14;
reconsider R =
[.(h /. i),(h /. (i + 1)).] as
Subset of
I[01] by A19, A36, A40, A42, A43, BORSUK_1:83, XXREAL_2:def 12;
reconsider w1 =
f . (h . i),
w2 =
f . (h . (i + 1)) as
Point of
(Euclid 2) by A38, A39, TOPREAL3:13;
A47:
h . i in R
by A40, A44, XXREAL_1:1;
h . (i + 1) in R
by A43, A44, XXREAL_1:1;
then A48:
(
w1 in f .: R &
w2 in f .: R )
by A37, A47, FUNCT_1:def 12;
reconsider W =
f .: R as
Subset of
(Euclid 2) by TOPREAL3:13;
(
dom f = [#] I[01] &
rng f = P )
by A1, FUNCT_2:def 1;
then A49:
P = f .: [.0 ,1.]
by BORSUK_1:83, RELAT_1:146;
0 in the
carrier of
I[01]
by BORSUK_1:86;
then
f . 0 in rng f
by A37, FUNCT_1:def 5;
then A50:
(
W-bound Pa <= p1 `1 &
p1 `1 <= E-bound Pa &
S-bound Pa <= p1 `2 &
p1 `2 <= N-bound Pa )
by A1, A7, A46, 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 A50, XXREAL_0:2;
then A51:
0 <= (E-bound Pa) - (W-bound Pa)
by XREAL_1:50;
S-bound Pa <= N-bound Pa
by A50, XXREAL_0:2;
then
0 <= (N-bound Pa) - (S-bound Pa)
by XREAL_1:50;
then A52:
((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa)) >= 0 + 0
by A51;
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 A54:
(
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) ;
A55:
dist x,
y = |.(pw1 - pw2).|
by JGRAPH_1:45;
A56:
|.(pw1 - pw2).| <= (abs ((pw1 `1 ) - (pw2 `1 ))) + (abs ((pw1 `2 ) - (pw2 `2 )))
by JGRAPH_1:49;
A57:
(
W-bound Pa <= pw1 `1 &
pw1 `1 <= E-bound Pa &
S-bound Pa <= pw1 `2 &
pw1 `2 <= N-bound Pa )
by A46, A54, PSCOMP_1:71;
A58:
(
W-bound Pa <= pw2 `1 &
pw2 `1 <= E-bound Pa &
S-bound Pa <= pw2 `2 &
pw2 `2 <= N-bound Pa )
by A46, A54, PSCOMP_1:71;
then A59:
abs ((pw1 `1 ) - (pw2 `1 )) <= (E-bound Pa) - (W-bound Pa)
by A57, JGRAPH_1:31;
abs ((pw1 `2 ) - (pw2 `2 )) <= (N-bound Pa) - (S-bound Pa)
by A57, A58, JGRAPH_1:31;
then A60:
(abs ((pw1 `1 ) - (pw2 `1 ))) + (abs ((pw1 `2 ) - (pw2 `2 ))) <= ((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))
by A59, 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 A60, XXREAL_0:2;
hence
dist x,
y <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1
by A55, A56, XXREAL_0:2;
:: thesis: verum
end;
then
W1 is
bounded
by A52, TBSP_1:def 9;
then A61:
W is
bounded
by A49, BORSUK_1:83, RELAT_1:156, TBSP_1:21;
A62:
diameter W < (min_dist_min P',Q') / 5
by A19, A20, A26, A27;
dist w1,
w2 <= diameter W
by A48, A61, TBSP_1:def 10;
then
dist w1,
w2 < (min_dist_min P',Q') / 5
by A62, XXREAL_0:2;
hence
|.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min P',Q') / 5
by A32, A34, JGRAPH_1:45;
:: thesis: verum
end;
A63:
len h1 >= 1
by A19, A20, XXREAL_0:2;
consider hb being FinSequence of REAL such that
A64:
( 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 = g .: R holds
diameter W < (min_dist_min P',Q') / 5 ) )
by A18, Th1;
A65:
1 <= len hb
by A64, XXREAL_0:2;
then A66:
1 in dom hb
by FINSEQ_3:27;
A67:
len hb in dom hb
by A65, FINSEQ_3:27;
deffunc H2( Nat) -> set = g . (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
A68:
( len h2' = len hb & ( for i being Nat st i in dom h2' holds
h2' . i = g . (hb . i) ) )
;
rng h2' c= the carrier of (TOP-REAL 2)
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 = g . (hb . i)
A77:
len h2 >= 1
by A64, A68, 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 A80:
i in dom h
by A20, FINSEQ_3:31;
i in dom h1'
by A79;
then
h1 . i = f . (h . i)
by A20;
then A81:
h1 /. i = f . (h . i)
by A79, PARTFUN1:def 8;
1
in dom h1'
by A63, FINSEQ_3:27;
then
h1 . 1
= f . (h . 1)
by A20;
then A82:
h1 /. 1
= f . (h . 1)
by A63, FINSEQ_4:24;
len h in dom h1'
by A20, A63, FINSEQ_3:27;
then
h1 . (len h1) = f . (h . (len h))
by A20;
then A83:
h1 /. (len h1) = f . (h . (len h))
by A63, FINSEQ_4:24;
A84:
h . i in rng h
by A80, FUNCT_1:def 5;
dom f = the
carrier of
I[01]
by FUNCT_2:def 1;
then
h1 /. i in rng f
by A19, A81, A84, FUNCT_1:def 5;
hence
(
(h1 /. 1) `1 <= (h1 /. i) `1 &
(h1 /. i) `1 <= (h1 /. (len h1)) `1 )
by A1, A3, A7, A19, A82, A83;
:: thesis: verum
end;
A85:
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) )
A89:
for i being Element of NAT st i in dom h1 holds
( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 )
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 A95:
( X_axis h1 lies_between (X_axis h1) . 1,(X_axis h1) . (len h1) & Y_axis h1 lies_between q1 `2 ,q2 `2 )
by A85, GOBOARD4:def 2;
A96:
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 A97:
i in dom hb
by A68, FINSEQ_1:def 3;
then A98:
h2 /. i = g . (hb . i)
by A74;
1
in Seg (len hb)
by A68, A77, FINSEQ_1:3;
then
1
in dom hb
by FINSEQ_1:def 3;
then A99:
h2 /. 1
= g . (hb . 1)
by A74;
len hb in Seg (len hb)
by A68, A77, FINSEQ_1:3;
then
len hb in dom hb
by FINSEQ_1:def 3;
then A100:
h2 /. (len h2) = g . (hb . (len hb))
by A68, A74;
A101:
hb . i in rng hb
by A97, FUNCT_1:def 5;
dom g = the
carrier of
I[01]
by FUNCT_2:def 1;
then
h2 /. i in rng g
by A64, A98, A101, FUNCT_1:def 5;
hence
(
(h2 /. 1) `2 <= (h2 /. i) `2 &
(h2 /. i) `2 <= (h2 /. (len h2)) `2 )
by A2, A6, A8, A64, A99, A100;
:: thesis: verum
end;
A102:
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) )
A106:
for i being Element of NAT st i in dom h2 holds
( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 )
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 A111:
( X_axis h2 lies_between p1 `1 ,p2 `1 & Y_axis h2 lies_between (Y_axis h2) . 1,(Y_axis h2) . (len h2) )
by A102, GOBOARD4:def 2;
A112:
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 A113:
( 1
<= i &
i + 1
<= len h2 )
;
:: thesis: |.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min P',Q') / 5
then A114:
i < len h2
by NAT_1:13;
A115:
1
< i + 1
by A113, NAT_1:13;
then A116:
i + 1
in dom h2'
by A113, FINSEQ_3:27;
i in dom h2'
by A113, A114, FINSEQ_3:27;
then A117:
h2' . i = g . (hb . i)
by A68;
then A118:
h2 /. i = g . (hb . i)
by A113, A114, FINSEQ_4:24;
A119:
h2' . (i + 1) = g . (hb . (i + 1))
by A68, A116;
h2 . (i + 1) = h2 /. (i + 1)
by A113, A115, FINSEQ_4:24;
then A120:
h2 /. (i + 1) = g . (hb . (i + 1))
by A68, A116;
i in Seg (len hb)
by A68, A113, A114, FINSEQ_1:3;
then A121:
i in dom hb
by FINSEQ_1:def 3;
then A122:
hb . i in rng hb
by FUNCT_1:def 5;
A123:
dom g = the
carrier of
I[01]
by FUNCT_2:def 1;
then A124:
h2' . i in rng g
by A64, A117, A122, FUNCT_1:def 5;
i + 1
in Seg (len hb)
by A68, A113, A115, 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 A64, A119, A123, FUNCT_1:def 5;
then A125:
g . (hb . (i + 1)) is
Element of
(TOP-REAL 2)
by A68, A116;
A126:
hb . i = hb /. i
by A68, A113, A114, FINSEQ_4:24;
i + 1
in Seg (len hb)
by A68, A113, A115, FINSEQ_1:3;
then A127:
i + 1
in dom hb
by FINSEQ_1:def 3;
then A128:
hb . (i + 1) in rng hb
by FUNCT_1:def 5;
A129:
hb . (i + 1) = hb /. (i + 1)
by A68, A113, A115, FINSEQ_4:24;
i < i + 1
by NAT_1:13;
then A130:
(
0 <= hb /. i &
hb /. i <= hb /. (i + 1) &
hb /. (i + 1) <= 1 )
by A64, A121, A122, A126, A127, A128, A129, 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) ;
A131:
[#] I[01] is
compact
by COMPTS_1:10;
g .: the
carrier of
I[01] = rng g
by FUNCT_2:45;
then A132:
Qa is
compact
by A2, A131, WEIERSTR:14;
reconsider Qa =
Qa as non
empty Subset of
(TOP-REAL 2) ;
reconsider R =
[.(hb /. i),(hb /. (i + 1)).] as
Subset of
I[01] by A64, A122, A126, A128, A129, BORSUK_1:83, XXREAL_2:def 12;
reconsider w1 =
g . (hb . i),
w2 =
g . (hb . (i + 1)) as
Point of
(Euclid 2) by A117, A124, A125, TOPREAL3:13;
A133:
hb . i in R
by A126, A130, XXREAL_1:1;
hb . (i + 1) in R
by A129, A130, XXREAL_1:1;
then A134:
(
w1 in g .: R &
w2 in g .: R )
by A123, A133, FUNCT_1:def 12;
reconsider W =
g .: R as
Subset of
(Euclid 2) by TOPREAL3:13;
(
dom g = [#] I[01] &
rng g = Q )
by A2, FUNCT_2:def 1;
then A135:
Q = g .: [.0 ,1.]
by BORSUK_1:83, RELAT_1:146;
0 in the
carrier of
I[01]
by BORSUK_1:86;
then
g . 0 in rng g
by A123, FUNCT_1:def 5;
then A136:
(
W-bound Qa <= q1 `1 &
q1 `1 <= E-bound Qa &
S-bound Qa <= q1 `2 &
q1 `2 <= N-bound Qa )
by A2, A8, A132, 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 A136, XXREAL_0:2;
then A137:
0 <= (E-bound Qa) - (W-bound Qa)
by XREAL_1:50;
S-bound Qa <= N-bound Qa
by A136, XXREAL_0:2;
then
0 <= (N-bound Qa) - (S-bound Qa)
by XREAL_1:50;
then A138:
((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa)) >= 0 + 0
by A137;
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 A140:
(
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) ;
A141:
dist x,
y = |.(pw1 - pw2).|
by JGRAPH_1:45;
A142:
|.(pw1 - pw2).| <= (abs ((pw1 `1 ) - (pw2 `1 ))) + (abs ((pw1 `2 ) - (pw2 `2 )))
by JGRAPH_1:49;
A143:
(
W-bound Qa <= pw1 `1 &
pw1 `1 <= E-bound Qa &
S-bound Qa <= pw1 `2 &
pw1 `2 <= N-bound Qa )
by A132, A140, PSCOMP_1:71;
A144:
(
W-bound Qa <= pw2 `1 &
pw2 `1 <= E-bound Qa &
S-bound Qa <= pw2 `2 &
pw2 `2 <= N-bound Qa )
by A132, A140, PSCOMP_1:71;
then A145:
abs ((pw1 `1 ) - (pw2 `1 )) <= (E-bound Qa) - (W-bound Qa)
by A143, JGRAPH_1:31;
abs ((pw1 `2 ) - (pw2 `2 )) <= (N-bound Qa) - (S-bound Qa)
by A143, A144, JGRAPH_1:31;
then A146:
(abs ((pw1 `1 ) - (pw2 `1 ))) + (abs ((pw1 `2 ) - (pw2 `2 ))) <= ((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))
by A145, 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 A146, XXREAL_0:2;
hence
dist x,
y <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1
by A141, A142, XXREAL_0:2;
:: thesis: verum
end;
then
W1 is
bounded
by A138, TBSP_1:def 9;
then A147:
W is
bounded
by A135, BORSUK_1:83, RELAT_1:156, TBSP_1:21;
A148:
diameter W < (min_dist_min P',Q') / 5
by A64, A68, A113, A114;
dist w1,
w2 <= diameter W
by A134, A147, TBSP_1:def 10;
then
dist w1,
w2 < (min_dist_min P',Q') / 5
by A148, XXREAL_0:2;
hence
|.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min P',Q') / 5
by A118, A120, JGRAPH_1:45;
:: thesis: verum
end;
consider f2 being FinSequence of (TOP-REAL 2) such that
A149:
( 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 A18, A25, A63, A95, JGRAPH_1:56;
A150:
len f2 >= 1
by A63, A149, XXREAL_0:2;
consider g2 being FinSequence of (TOP-REAL 2) such that
A151:
( 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 A18, A77, A111, A112, JGRAPH_1:57;
A152:
len g2 >= 1
by A77, A151, XXREAL_0:2;
A153:
1 in dom h1'
by A63, FINSEQ_3:27;
A154:
len h in dom h1'
by A20, A63, FINSEQ_3:27;
A155:
h1 . 1 = f . (h . 1)
by A20, A153;
A156:
h1 . 1 = h1 /. 1
by A63, FINSEQ_4:24;
A157:
h1 . (len h1) = h1 /. (len h1)
by A63, FINSEQ_4:24;
A158:
f2 . 1 = f2 /. 1
by A150, FINSEQ_4:24;
A159:
f2 . (len f2) = f2 /. (len f2)
by A150, FINSEQ_4:24;
A160:
(X_axis f2) . 1 = p1 `1
by A7, A19, A149, A150, A155, A158, JGRAPH_1:59;
h1 /. (len h1) = p2
by A7, A19, A20, A154, A157;
then A161:
(X_axis f2) . (len f2) = p2 `1
by A149, A150, A157, A159, JGRAPH_1:59;
A162:
h2 /. 1 = q1
by A8, A64, A66, A74;
A163:
h2 . 1 = h2 /. 1
by A65, A68, FINSEQ_4:24;
A164:
h2 . (len h2) = h2 /. (len h2)
by A65, A68, FINSEQ_4:24;
g2 /. 1 = g2 . 1
by A152, FINSEQ_4:24;
then A165:
(Y_axis g2) . 1 = q1 `2
by A151, A152, A162, A163, JGRAPH_1:60;
A166:
g2 /. (len g2) = g2 . (len g2)
by A152, FINSEQ_4:24;
g2 . (len g2) = q2
by A8, A64, A67, A68, A74, A151, A164;
then A167:
(Y_axis g2) . (len g2) = q2 `2
by A152, A166, JGRAPH_1:60;
A168: (X_axis f2) . 1 =
(h1 /. 1) `1
by A149, A150, A156, A158, JGRAPH_1:59
.=
(X_axis h1) . 1
by A63, JGRAPH_1:59
;
A169: (X_axis f2) . (len f2) =
(h1 /. (len h1)) `1
by A149, A150, A157, A159, JGRAPH_1:59
.=
(X_axis h1) . (len h1)
by A63, JGRAPH_1:59
;
g2 . 1 = g2 /. 1
by A152, FINSEQ_4:24;
then A170: (Y_axis g2) . 1 =
(h2 /. 1) `2
by A151, A152, A163, JGRAPH_1:60
.=
(Y_axis h2) . 1
by A77, JGRAPH_1:60
;
g2 . (len g2) = g2 /. (len g2)
by A152, FINSEQ_4:24;
then A171: (Y_axis g2) . (len g2) =
(h2 /. (len h2)) `2
by A151, A152, A164, JGRAPH_1:60
.=
(Y_axis h2) . (len h2)
by A77, JGRAPH_1:60
;
5 <= len f2
by A19, A20, A149, XXREAL_0:2;
then A172:
2 <= len f2
by XXREAL_0:2;
5 <= len g2
by A64, A68, A151, XXREAL_0:2;
then A173:
2 <= len g2
by XXREAL_0:2;
A174:
1 <= len h
by A19, XXREAL_0:2;
then
1 in dom h1'
by A20, FINSEQ_3:27;
then A175:
h1 /. 1 = f . (h . 1)
by A20, A156;
A176:
len h in dom h1'
by A174, A20, FINSEQ_3:27;
now per cases
( p1 = p2 or p1 <> p2 )
;
case A177:
p1 = p2
;
:: thesis: contradictionA178:
for
q being
Point of
(TOP-REAL 2) st
q in Q holds
q `1 = p1 `1
0 in the
carrier of
I[01]
by BORSUK_1:86;
then A179:
0 in dom g
by FUNCT_2:def 1;
then A180:
q1 in Q
by A2, A8, FUNCT_1:12;
1
in the
carrier of
I[01]
by BORSUK_1:86;
then
1
in dom g
by FUNCT_2:def 1;
then A181:
q2 in Q
by A2, A8, FUNCT_1:12;
0 in the
carrier of
I[01]
by BORSUK_1:86;
then
0 in dom f
by FUNCT_2:def 1;
then A182:
p1 in P
by A1, A7, FUNCT_1:12;
A183:
now assume A184:
q1 `2 = q2 `2
;
:: thesis: contradiction
(
q1 `2 <= p1 `2 &
p1 `2 <= q2 `2 )
by A5, A182;
then A185:
p1 `2 = q1 `2
by A184, XXREAL_0:1;
q1 `1 = p1 `1
by A2, A8, A178, A179, FUNCT_1:12;
then
q1 = p1
by A185, TOPREAL3:11;
hence
contradiction
by A16, A180, A182, XBOOLE_0:def 4;
:: thesis: verum end; A186:
Q c= LSeg q1,
q2
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in Q or z in LSeg q1,q2 )
assume A187:
z in Q
;
:: thesis: z in LSeg q1,q2
then reconsider qz =
z as
Point of
(TOP-REAL 2) ;
A188:
(
p1 `1 <= qz `1 &
qz `1 <= p2 `1 )
by A4, A187;
(
p1 `1 <= q1 `1 &
q1 `1 <= p2 `1 )
by A4, A180;
then A189:
p1 `1 = q1 `1
by A177, XXREAL_0:1;
(
p1 `1 <= q2 `1 &
q2 `1 <= p2 `1 )
by A4, A181;
then A190:
p1 `1 = q2 `1
by A177, XXREAL_0:1;
A191:
(
q1 `2 <= qz `2 &
qz `2 <= q2 `2 )
by A6, A187;
then
q2 `2 >= q1 `2
by XXREAL_0:2;
then
q2 `2 > q1 `2
by A183, XXREAL_0:1;
then A192:
(q2 `2 ) - (q1 `2 ) > 0
by XREAL_1:52;
A193:
(qz `2 ) - (q1 `2 ) >= 0
by A191, XREAL_1:50;
set ln =
((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ));
A194:
((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )) >= 0
by A192, A193;
(qz `2 ) - (q1 `2 ) <= (q2 `2 ) - (q1 `2 )
by A191, XREAL_1:15;
then
((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )) <= ((q2 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))
by A192, XREAL_1:74;
then A195:
((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )) <= 1
by A192, XCMPLX_1:60;
A196:
(q2 `2 ) - (q1 `2 ) <> 0
by A183;
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:121
.=
((q2 `2 ) - (qz `2 )) / ((q2 `2 ) - (q1 `2 ))
;
then A197:
(1 - (((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) * (q1 `2 ) =
(((q2 `2 ) - (qz `2 )) * (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))
by XCMPLX_1:75
.=
(((q2 `2 ) * (q1 `2 )) - ((qz `2 ) * (q1 `2 ))) / ((q2 `2 ) - (q1 `2 ))
;
A198:
(((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) * (q2 `2 ) =
(((qz `2 ) - (q1 `2 )) * (q2 `2 )) / ((q2 `2 ) - (q1 `2 ))
by XCMPLX_1:75
.=
(((qz `2 ) * (q2 `2 )) - ((q1 `2 ) * (q2 `2 ))) / ((q2 `2 ) - (q1 `2 ))
;
A199:
(((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:7
.=
((1 - (((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) * (q1 `1 )) + (((((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) * q2) `1 )
by TOPREAL3:9
.=
((1 - (((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) * (p1 `1 )) + ((((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) * (p1 `1 ))
by A189, A190, TOPREAL3:9
.=
qz `1
by A177, A188, XXREAL_0:1
;
(((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:7
.=
((1 - (((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) * (q1 `2 )) + (((((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) * q2) `2 )
by TOPREAL3:9
.=
((1 - (((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) * (q1 `2 )) + ((((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) * (q2 `2 ))
by TOPREAL3:9
.=
((((q2 `2 ) * (q1 `2 )) - ((qz `2 ) * (q1 `2 ))) + (((qz `2 ) * (q2 `2 )) - ((q1 `2 ) * (q2 `2 )))) / ((q2 `2 ) - (q1 `2 ))
by A197, A198, XCMPLX_1:63
.=
((qz `2 ) * ((q2 `2 ) - (q1 `2 ))) / ((q2 `2 ) - (q1 `2 ))
.=
(qz `2 ) * (((q2 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))
by XCMPLX_1:75
.=
(qz `2 ) * 1
by A196, XCMPLX_1:60
.=
qz `2
;
then
((1 - (((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) * q1) + ((((qz `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) * q2) = qz
by A199, TOPREAL3:11;
then
z in { (((1 - lambda) * q1) + (lambda * q2)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) }
by A194, A195;
hence
z in LSeg q1,
q2
by TOPREAL1:def 3;
:: thesis: verum
end;
p1 in LSeg q1,
q2
proof
0 in the
carrier of
I[01]
by BORSUK_1:86;
then
0 in dom g
by FUNCT_2:def 1;
then
q1 in Q
by A2, A8, FUNCT_1:12;
then
(
p1 `1 <= q1 `1 &
q1 `1 <= p2 `1 )
by A4;
then A200:
p1 `1 = q1 `1
by A177, XXREAL_0:1;
1
in the
carrier of
I[01]
by BORSUK_1:86;
then
1
in dom g
by FUNCT_2:def 1;
then
g . 1
in rng g
by FUNCT_1:12;
then
(
p1 `1 <= q2 `1 &
q2 `1 <= p2 `1 )
by A2, A4, A8;
then A201:
p1 `1 = q2 `1
by A177, XXREAL_0:1;
0 in the
carrier of
I[01]
by BORSUK_1:86;
then
0 in dom f
by FUNCT_2:def 1;
then
f . 0 in rng f
by FUNCT_1:12;
then A202:
(
q1 `2 <= p1 `2 &
p1 `2 <= q2 `2 )
by A1, A5, A7;
then
q2 `2 >= q1 `2
by XXREAL_0:2;
then
q2 `2 > q1 `2
by A183, XXREAL_0:1;
then A203:
(q2 `2 ) - (q1 `2 ) > 0
by XREAL_1:52;
A204:
(p1 `2 ) - (q1 `2 ) >= 0
by A202, XREAL_1:50;
set ln =
((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ));
A205:
((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )) >= 0
by A203, A204;
(p1 `2 ) - (q1 `2 ) <= (q2 `2 ) - (q1 `2 )
by A202, XREAL_1:15;
then
((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )) <= ((q2 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))
by A203, XREAL_1:74;
then A206:
((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )) <= 1
by A203, XCMPLX_1:60;
A207:
(q2 `2 ) - (q1 `2 ) <> 0
by A183;
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:121
.=
((q2 `2 ) - (p1 `2 )) / ((q2 `2 ) - (q1 `2 ))
;
then A208:
(1 - (((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) * (q1 `2 ) =
(((q2 `2 ) - (p1 `2 )) * (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))
by XCMPLX_1:75
.=
(((q2 `2 ) * (q1 `2 )) - ((p1 `2 ) * (q1 `2 ))) / ((q2 `2 ) - (q1 `2 ))
;
A209:
(((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) * (q2 `2 ) =
(((p1 `2 ) - (q1 `2 )) * (q2 `2 )) / ((q2 `2 ) - (q1 `2 ))
by XCMPLX_1:75
.=
(((p1 `2 ) * (q2 `2 )) - ((q1 `2 ) * (q2 `2 ))) / ((q2 `2 ) - (q1 `2 ))
;
A210:
(((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:7
.=
((1 - (((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) * (q1 `1 )) + (((((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) * q2) `1 )
by TOPREAL3:9
.=
((1 - (((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) * (p1 `1 )) + ((((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) * (p1 `1 ))
by A200, A201, TOPREAL3:9
.=
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:7
.=
((1 - (((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) * (q1 `2 )) + (((((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) * q2) `2 )
by TOPREAL3:9
.=
((1 - (((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) * (q1 `2 )) + ((((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) * (q2 `2 ))
by TOPREAL3:9
.=
((((q2 `2 ) * (q1 `2 )) - ((p1 `2 ) * (q1 `2 ))) + (((p1 `2 ) * (q2 `2 )) - ((q1 `2 ) * (q2 `2 )))) / ((q2 `2 ) - (q1 `2 ))
by A208, A209, XCMPLX_1:63
.=
((p1 `2 ) * ((q2 `2 ) - (q1 `2 ))) / ((q2 `2 ) - (q1 `2 ))
.=
(p1 `2 ) * (((q2 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))
by XCMPLX_1:75
.=
(p1 `2 ) * 1
by A207, XCMPLX_1:60
.=
p1 `2
;
then
((1 - (((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 )))) * q1) + ((((p1 `2 ) - (q1 `2 )) / ((q2 `2 ) - (q1 `2 ))) * q2) = p1
by A210, TOPREAL3:11;
then
p1 in { (((1 - lambda) * q1) + (lambda * q2)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) }
by A205, A206;
hence
p1 in LSeg q1,
q2
by TOPREAL1:def 3;
:: thesis: verum
end; then
p1 in Q
by A2, A186, Th3;
hence
contradiction
by A13, A16, XBOOLE_0:def 4;
:: thesis: verum end; case
p1 <> p2
;
:: thesis: contradictionthen A211:
f2 /. 1
<> f2 /. (len f2)
by A7, A19, A20, A149, A156, A158, A159, A175, A176;
A212:
now assume A213:
q1 = q2
;
:: thesis: contradictionA214:
for
p being
Point of
(TOP-REAL 2) st
p in P holds
p `2 = q1 `2
0 in the
carrier of
I[01]
by BORSUK_1:86;
then A215:
0 in dom f
by FUNCT_2:def 1;
then A216:
p1 in P
by A1, A7, FUNCT_1:12;
1
in the
carrier of
I[01]
by BORSUK_1:86;
then
1
in dom f
by FUNCT_2:def 1;
then A217:
p2 in P
by A1, A7, FUNCT_1:12;
0 in the
carrier of
I[01]
by BORSUK_1:86;
then
0 in dom g
by FUNCT_2:def 1;
then A218:
q1 in Q
by A2, A8, FUNCT_1:12;
A219:
now assume A220:
p1 `1 = p2 `1
;
:: thesis: contradiction
(
p1 `1 <= q1 `1 &
q1 `1 <= p2 `1 )
by A4, A218;
then A221:
q1 `1 = p1 `1
by A220, XXREAL_0:1;
p1 `2 = q1 `2
by A1, A7, A214, A215, FUNCT_1:12;
then
p1 = q1
by A221, TOPREAL3:11;
hence
contradiction
by A16, A216, A218, XBOOLE_0:def 4;
:: thesis: verum end; A222:
P c= LSeg p1,
p2
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in P or z in LSeg p1,p2 )
assume A223:
z in P
;
:: thesis: z in LSeg p1,p2
then reconsider pz =
z as
Point of
(TOP-REAL 2) ;
A224:
(
q1 `2 <= pz `2 &
pz `2 <= q2 `2 )
by A5, A223;
(
q1 `2 <= p1 `2 &
p1 `2 <= q2 `2 )
by A5, A216;
then A225:
q1 `2 = p1 `2
by A213, XXREAL_0:1;
(
q1 `2 <= p2 `2 &
p2 `2 <= q2 `2 )
by A5, A217;
then A226:
q1 `2 = p2 `2
by A213, XXREAL_0:1;
A227:
(
p1 `1 <= pz `1 &
pz `1 <= p2 `1 )
by A3, A223;
then
p2 `1 >= p1 `1
by XXREAL_0:2;
then
p2 `1 > p1 `1
by A219, XXREAL_0:1;
then A228:
(p2 `1 ) - (p1 `1 ) > 0
by XREAL_1:52;
A229:
(pz `1 ) - (p1 `1 ) >= 0
by A227, XREAL_1:50;
set ln =
((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ));
A230:
((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )) >= 0
by A228, A229;
(pz `1 ) - (p1 `1 ) <= (p2 `1 ) - (p1 `1 )
by A227, XREAL_1:15;
then
((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )) <= ((p2 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))
by A228, XREAL_1:74;
then A231:
((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )) <= 1
by A228, XCMPLX_1:60;
A232:
(p2 `1 ) - (p1 `1 ) <> 0
by A219;
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:121
.=
((p2 `1 ) - (pz `1 )) / ((p2 `1 ) - (p1 `1 ))
;
then A233:
(1 - (((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * (p1 `1 ) =
(((p2 `1 ) - (pz `1 )) * (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))
by XCMPLX_1:75
.=
(((p2 `1 ) * (p1 `1 )) - ((pz `1 ) * (p1 `1 ))) / ((p2 `1 ) - (p1 `1 ))
;
A234:
(((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * (p2 `1 ) =
(((pz `1 ) - (p1 `1 )) * (p2 `1 )) / ((p2 `1 ) - (p1 `1 ))
by XCMPLX_1:75
.=
(((pz `1 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `1 ))) / ((p2 `1 ) - (p1 `1 ))
;
A235:
(((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:7
.=
((1 - (((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * (p1 `2 )) + (((((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * p2) `2 )
by TOPREAL3:9
.=
((1 - (((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * (q1 `2 )) + ((((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * (q1 `2 ))
by A225, A226, TOPREAL3:9
.=
pz `2
by A213, A224, XXREAL_0:1
;
(((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:7
.=
((1 - (((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * (p1 `1 )) + (((((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * p2) `1 )
by TOPREAL3:9
.=
((1 - (((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * (p1 `1 )) + ((((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * (p2 `1 ))
by TOPREAL3:9
.=
((((p2 `1 ) * (p1 `1 )) - ((pz `1 ) * (p1 `1 ))) + (((pz `1 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `1 )))) / ((p2 `1 ) - (p1 `1 ))
by A233, A234, XCMPLX_1:63
.=
((pz `1 ) * ((p2 `1 ) - (p1 `1 ))) / ((p2 `1 ) - (p1 `1 ))
.=
(pz `1 ) * (((p2 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))
by XCMPLX_1:75
.=
(pz `1 ) * 1
by A232, XCMPLX_1:60
.=
pz `1
;
then
((1 - (((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * p1) + ((((pz `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * p2) = pz
by A235, TOPREAL3:11;
then
z in { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) }
by A230, A231;
hence
z in LSeg p1,
p2
by TOPREAL1:def 3;
:: thesis: verum
end;
q1 in LSeg p1,
p2
proof
0 in the
carrier of
I[01]
by BORSUK_1:86;
then
0 in dom f
by FUNCT_2:def 1;
then
f . 0 in rng f
by FUNCT_1:12;
then
(
q1 `2 <= p1 `2 &
p1 `2 <= q2 `2 )
by A1, A5, A7;
then A236:
q1 `2 = p1 `2
by A213, XXREAL_0:1;
1
in the
carrier of
I[01]
by BORSUK_1:86;
then
1
in dom f
by FUNCT_2:def 1;
then
f . 1
in rng f
by FUNCT_1:12;
then
(
q1 `2 <= p2 `2 &
p2 `2 <= q2 `2 )
by A1, A5, A7;
then A237:
q1 `2 = p2 `2
by A213, XXREAL_0:1;
0 in the
carrier of
I[01]
by BORSUK_1:86;
then
0 in dom g
by FUNCT_2:def 1;
then
g . 0 in rng g
by FUNCT_1:12;
then A238:
(
p1 `1 <= q1 `1 &
q1 `1 <= p2 `1 )
by A2, A4, A8;
then
p2 `1 >= p1 `1
by XXREAL_0:2;
then
p2 `1 > p1 `1
by A219, XXREAL_0:1;
then A239:
(p2 `1 ) - (p1 `1 ) > 0
by XREAL_1:52;
A240:
(q1 `1 ) - (p1 `1 ) >= 0
by A238, XREAL_1:50;
set ln =
((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ));
A241:
((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )) >= 0
by A239, A240;
(q1 `1 ) - (p1 `1 ) <= (p2 `1 ) - (p1 `1 )
by A238, XREAL_1:15;
then
((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )) <= ((p2 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))
by A239, XREAL_1:74;
then A242:
((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )) <= 1
by A239, XCMPLX_1:60;
A243:
(p2 `1 ) - (p1 `1 ) <> 0
by A219;
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:121
.=
((p2 `1 ) - (q1 `1 )) / ((p2 `1 ) - (p1 `1 ))
;
then A244:
(1 - (((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * (p1 `1 ) =
(((p2 `1 ) - (q1 `1 )) * (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))
by XCMPLX_1:75
.=
(((p2 `1 ) * (p1 `1 )) - ((q1 `1 ) * (p1 `1 ))) / ((p2 `1 ) - (p1 `1 ))
;
A245:
(((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * (p2 `1 ) =
(((q1 `1 ) - (p1 `1 )) * (p2 `1 )) / ((p2 `1 ) - (p1 `1 ))
by XCMPLX_1:75
.=
(((q1 `1 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `1 ))) / ((p2 `1 ) - (p1 `1 ))
;
A246:
(((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:7
.=
((1 - (((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * (p1 `2 )) + (((((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * p2) `2 )
by TOPREAL3:9
.=
((1 - (((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * (q1 `2 )) + ((((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * (q1 `2 ))
by A236, A237, TOPREAL3:9
;
(((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:7
.=
((1 - (((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * (p1 `1 )) + (((((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * p2) `1 )
by TOPREAL3:9
.=
((1 - (((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * (p1 `1 )) + ((((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * (p2 `1 ))
by TOPREAL3:9
.=
((((p2 `1 ) * (p1 `1 )) - ((q1 `1 ) * (p1 `1 ))) + (((q1 `1 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `1 )))) / ((p2 `1 ) - (p1 `1 ))
by A244, A245, XCMPLX_1:63
.=
((q1 `1 ) * ((p2 `1 ) - (p1 `1 ))) / ((p2 `1 ) - (p1 `1 ))
.=
(q1 `1 ) * (((p2 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))
by XCMPLX_1:75
.=
(q1 `1 ) * 1
by A243, XCMPLX_1:60
;
then
((1 - (((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 )))) * p1) + ((((q1 `1 ) - (p1 `1 )) / ((p2 `1 ) - (p1 `1 ))) * p2) = q1
by A246, TOPREAL3:11;
then
q1 in { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) }
by A241, A242;
hence
q1 in LSeg p1,
p2
by TOPREAL1:def 3;
:: thesis: verum
end; then
q1 in P
by A1, A222, Th3;
hence
contradiction
by A14, A16, XBOOLE_0:def 4;
:: thesis: verum end; A247:
1
<= len hb
by A64, XXREAL_0:2;
then
1
in dom hb
by FINSEQ_3:27;
then A248:
h2 /. 1
= g . (hb . 1)
by A74;
len hb in dom hb
by A247, FINSEQ_3:27;
then
g2 . 1
<> g2 . (len g2)
by A8, A64, A68, A74, A151, A163, A164, A212, A248;
then
L~ f2 meets L~ g2
by A149, A151, A158, A159, A160, A161, A165, A167, A168, A169, A170, A171, A172, A173, A211, JGRAPH_1:30;
then consider s being
set such that A249:
(
s in L~ f2 &
s in L~ g2 )
by XBOOLE_0:3;
reconsider ps =
s as
Point of
(TOP-REAL 2) by A249;
ps in union { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) }
by A249, TOPREAL1:def 6;
then consider x being
set such that A250:
(
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 A251:
(
x = LSeg f2,
i & 1
<= i &
i + 1
<= len f2 )
by A250;
A252:
LSeg f2,
i = LSeg (f2 /. i),
(f2 /. (i + 1))
by A251, TOPREAL1:def 5;
i < len f2
by A251, NAT_1:13;
then
i in dom f2
by A251, FINSEQ_3:27;
then consider k being
Element of
NAT such that A253:
(
k in dom h1 &
|.((f2 /. i) - (h1 /. k)).| < (min_dist_min P',Q') / 5 )
by A149;
A254:
|.(ps - (f2 /. i)).| <= |.((f2 /. i) - (f2 /. (i + 1))).|
by A250, A251, A252, JGRAPH_1:53;
|.((f2 /. i) - (f2 /. (i + 1))).| < (min_dist_min P',Q') / 5
by A149, A251;
then A255:
|.(ps - (f2 /. i)).| < (min_dist_min P',Q') / 5
by A254, XXREAL_0:2;
A256:
|.(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 A253, A255, XREAL_1:10;
then A257:
|.(ps - (h1 /. k)).| < ((min_dist_min P',Q') / 5) + ((min_dist_min P',Q') / 5)
by A256, XXREAL_0:2;
A258:
k in Seg (len h1)
by A253, FINSEQ_1:def 3;
then A259:
k in dom h1'
by FINSEQ_1:def 3;
A260:
k in dom h
by A20, A258, FINSEQ_1:def 3;
( 1
<= k &
k <= len h1 )
by A258, FINSEQ_1:3;
then
h1 . k = h1 /. k
by FINSEQ_4:24;
then A261:
h1 /. k = f . (h . k)
by A20, A259;
A262:
h . k in rng h
by A260, FUNCT_1:def 5;
dom f = the
carrier of
I[01]
by FUNCT_2:def 1;
then A263:
h1 /. k in P
by A1, A19, A261, A262, FUNCT_1:def 5;
reconsider p11 =
h1 /. k as
Point of
(TOP-REAL 2) ;
A264:
|.(p11 - ps).| < ((min_dist_min P',Q') / 5) + ((min_dist_min P',Q') / 5)
by A257, TOPRNS_1:28;
ps in union { (LSeg g2,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len g2 ) }
by A249, TOPREAL1:def 6;
then consider y being
set such that A265:
(
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 A266:
(
y = LSeg g2,
j & 1
<= j &
j + 1
<= len g2 )
by A265;
A267:
(
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 A265, A266, 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 A265, A266, NAT_1:13, TOPREAL1:def 5;
then
j in dom g2
by FINSEQ_3:27;
then consider k' being
Element of
NAT such that A268:
(
k' in dom h2 &
|.((g2 /. j) - (h2 /. k')).| < (min_dist_min P',Q') / 5 )
by A151;
A269:
|.(ps - (g2 /. j)).| <= |.((g2 /. j) - (g2 /. (j + 1))).|
by A267, JGRAPH_1:53;
|.((g2 /. j) - (g2 /. (j + 1))).| < (min_dist_min P',Q') / 5
by A151, A266;
then A270:
|.(ps - (g2 /. j)).| < (min_dist_min P',Q') / 5
by A269, XXREAL_0:2;
A271:
|.(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 A268, A270, XREAL_1:10;
then A272:
|.(ps - (h2 /. k')).| < ((min_dist_min P',Q') / 5) + ((min_dist_min P',Q') / 5)
by A271, XXREAL_0:2;
k' in Seg (len h2)
by A268, FINSEQ_1:def 3;
then
k' in dom hb
by A68, FINSEQ_1:def 3;
then A273:
(
hb . k' in rng hb &
h2 /. k' = g . (hb . k') &
k' in dom hb )
by A74, FUNCT_1:def 5;
dom g = the
carrier of
I[01]
by FUNCT_2:def 1;
then A274:
(
Q <> {} (TOP-REAL 2) &
h2 /. k' in rng g &
hb . k' in dom g )
by A64, A273, FUNCT_1:def 5;
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 A2, A15, A263, A274, WEIERSTR:40;
then A275:
(
|.(p11 - q11).| <= |.(p11 - ps).| + |.(ps - q11).| &
min_dist_min P',
Q' <= |.(p11 - q11).| )
by JGRAPH_1:45, 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 A264, A272, 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 A275, XXREAL_0:2;
then
min_dist_min P',
Q' < 4
* ((min_dist_min P',Q') / 5)
by A275, 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 A18, XREAL_1:141;
then
4
- 5
> 0
by A18;
hence
contradiction
;
:: thesis: verum end;
hence
contradiction
; :: thesis: verum