let C be compact non horizontal non vertical Subset of (TOP-REAL 2); for r, t being real number st r > 0 & t > 0 holds
ex n being Element of NAT st
( 1 < n & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < t )
let r, t be real number ; ( r > 0 & t > 0 implies ex n being Element of NAT st
( 1 < n & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < t ) )
assume that
A1:
r > 0
and
A2:
t > 0
; ex n being Element of NAT st
( 1 < n & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < t )
set n = N-bound C;
set e = E-bound C;
set s = S-bound C;
set w = W-bound C;
set a = (abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1;
set b = (abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1;
take i = (max ((abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1),((abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1)) + 1; ( 1 < i & dist ((Gauge C,i) * 1,1),((Gauge C,i) * 1,2) < r & dist ((Gauge C,i) * 1,1),((Gauge C,i) * 2,1) < t )
A3:
2 to_power i > 0
by POWER:39;
then A4:
2 |^ i > 0
by POWER:46;
[\(log 2,(((N-bound C) - (S-bound C)) / r))/] <= abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]
by ABSVALUE:11;
then A5:
[\(log 2,(((N-bound C) - (S-bound C)) / r))/] + 1 <= (abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1
by XREAL_1:8;
[\(log 2,(((N-bound C) - (S-bound C)) / r))/] > (log 2,(((N-bound C) - (S-bound C)) / r)) - 1
by INT_1:def 4;
then
[\(log 2,(((N-bound C) - (S-bound C)) / r))/] + 1 > ((log 2,(((N-bound C) - (S-bound C)) / r)) - 1) + 1
by XREAL_1:8;
then A6:
(abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1 > ((log 2,(((N-bound C) - (S-bound C)) / r)) - 1) + 1
by A5, XXREAL_0:2;
(abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1 <= max ((abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1),((abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1)
by XXREAL_0:25;
then A7:
((abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1) + 1 <= (max ((abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1),((abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1)) + 1
by XREAL_1:8;
(abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1 < ((abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1) + 1
by XREAL_1:31;
then
i > (abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1
by A7, XXREAL_0:2;
then
i > log 2,(((N-bound C) - (S-bound C)) / r)
by A6, XXREAL_0:2;
then
log 2,(2 to_power i) > log 2,(((N-bound C) - (S-bound C)) / r)
by A3, POWER:def 3;
then
2 to_power i > ((N-bound C) - (S-bound C)) / r
by A3, PRE_FF:12;
then
2 |^ i > ((N-bound C) - (S-bound C)) / r
by POWER:46;
then
(2 |^ i) * r > (((N-bound C) - (S-bound C)) / r) * r
by A1, XREAL_1:70;
then
(2 |^ i) * r > (N-bound C) - (S-bound C)
by A1, XCMPLX_1:88;
then
((2 |^ i) * r) / (2 |^ i) > ((N-bound C) - (S-bound C)) / (2 |^ i)
by A4, XREAL_1:76;
then A8:
((N-bound C) - (S-bound C)) / (2 |^ i) < r
by A4, XCMPLX_1:90;
( (abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1 >= 0 + 1 & max ((abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1),((abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1) >= (abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1 )
by XREAL_1:9, XXREAL_0:25;
then
max ((abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1),((abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1) >= 1
by XXREAL_0:2;
then
(max ((abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1),((abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1)) + 1 >= 1 + 1
by XREAL_1:9;
hence
1 < i
by XXREAL_0:2; ( dist ((Gauge C,i) * 1,1),((Gauge C,i) * 1,2) < r & dist ((Gauge C,i) * 1,1),((Gauge C,i) * 2,1) < t )
A9:
len (Gauge C,i) >= 4
by JORDAN8:13;
then A10:
1 <= len (Gauge C,i)
by XXREAL_0:2;
[\(log 2,(((E-bound C) - (W-bound C)) / t))/] <= abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]
by ABSVALUE:11;
then A11:
[\(log 2,(((E-bound C) - (W-bound C)) / t))/] + 1 <= (abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1
by XREAL_1:8;
[\(log 2,(((E-bound C) - (W-bound C)) / t))/] > (log 2,(((E-bound C) - (W-bound C)) / t)) - 1
by INT_1:def 4;
then
[\(log 2,(((E-bound C) - (W-bound C)) / t))/] + 1 > ((log 2,(((E-bound C) - (W-bound C)) / t)) - 1) + 1
by XREAL_1:8;
then A12:
(abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1 > ((log 2,(((E-bound C) - (W-bound C)) / t)) - 1) + 1
by A11, XXREAL_0:2;
(abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1 <= max ((abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1),((abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1)
by XXREAL_0:25;
then A13:
((abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1) + 1 <= (max ((abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1),((abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1)) + 1
by XREAL_1:8;
(abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1 < ((abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1) + 1
by XREAL_1:31;
then
i > (abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1
by A13, XXREAL_0:2;
then
i > log 2,(((E-bound C) - (W-bound C)) / t)
by A12, XXREAL_0:2;
then
log 2,(2 to_power i) > log 2,(((E-bound C) - (W-bound C)) / t)
by A3, POWER:def 3;
then
2 to_power i > ((E-bound C) - (W-bound C)) / t
by A3, PRE_FF:12;
then
2 |^ i > ((E-bound C) - (W-bound C)) / t
by POWER:46;
then
(2 |^ i) * t > (((E-bound C) - (W-bound C)) / t) * t
by A2, XREAL_1:70;
then
(2 |^ i) * t > (E-bound C) - (W-bound C)
by A2, XCMPLX_1:88;
then
((2 |^ i) * t) / (2 |^ i) > ((E-bound C) - (W-bound C)) / (2 |^ i)
by A4, XREAL_1:76;
then A14:
((E-bound C) - (W-bound C)) / (2 |^ i) < t
by A4, XCMPLX_1:90;
A15:
len (Gauge C,i) = width (Gauge C,i)
by JORDAN8:def 1;
then A16:
[1,1] in Indices (Gauge C,i)
by A10, MATRIX_1:37;
A17:
1 + 1 <= width (Gauge C,i)
by A15, A9, XXREAL_0:2;
then A18:
[1,(1 + 1)] in Indices (Gauge C,i)
by A10, MATRIX_1:37;
[(1 + 1),1] in Indices (Gauge C,i)
by A15, A10, A17, MATRIX_1:37;
hence
( dist ((Gauge C,i) * 1,1),((Gauge C,i) * 1,2) < r & dist ((Gauge C,i) * 1,1),((Gauge C,i) * 2,1) < t )
by A8, A14, A16, A18, Th19, Th20; verum