let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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: (abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1 >= 0 + 1 by XREAL_1:9;
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 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 A3, 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; :: thesis: ( dist ((Gauge C,i) * 1,1),((Gauge C,i) * 1,2) < r & dist ((Gauge C,i) * 1,1),((Gauge C,i) * 2,1) < t )
( (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) & (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 A4: ( ((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 & ((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,(((N-bound C) - (S-bound C)) / r))/]) + 1 < ((abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1) + 1 & (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 A5: ( i > (abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1 & i > (abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1 ) by A4, XXREAL_0:2;
A6: 2 to_power i > 0 by POWER:39;
then A7: 2 |^ i > 0 by POWER:46;
( [\(log 2,(((N-bound C) - (S-bound C)) / r))/] > (log 2,(((N-bound C) - (S-bound C)) / r)) - 1 & [\(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 A8: ( [\(log 2,(((N-bound C) - (S-bound C)) / r))/] + 1 > ((log 2,(((N-bound C) - (S-bound C)) / r)) - 1) + 1 & [\(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;
( [\(log 2,(((N-bound C) - (S-bound C)) / r))/] <= abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/] & [\(log 2,(((E-bound C) - (W-bound C)) / t))/] <= abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/] ) by ABSVALUE:11;
then ( [\(log 2,(((N-bound C) - (S-bound C)) / r))/] + 1 <= (abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1 & [\(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;
then ( (abs [\(log 2,(((N-bound C) - (S-bound C)) / r))/]) + 1 > ((log 2,(((N-bound C) - (S-bound C)) / r)) - 1) + 1 & (abs [\(log 2,(((E-bound C) - (W-bound C)) / t))/]) + 1 > ((log 2,(((E-bound C) - (W-bound C)) / t)) - 1) + 1 ) by A8, XXREAL_0:2;
then ( i > log 2,(((N-bound C) - (S-bound C)) / r) & i > log 2,(((E-bound C) - (W-bound C)) / t) ) by A5, XXREAL_0:2;
then ( log 2,(2 to_power i) > log 2,(((N-bound C) - (S-bound C)) / r) & log 2,(2 to_power i) > log 2,(((E-bound C) - (W-bound C)) / t) ) by A6, POWER:def 3;
then ( 2 to_power i > ((N-bound C) - (S-bound C)) / r & 2 to_power i > ((E-bound C) - (W-bound C)) / t ) by A6, PRE_FF:12;
then ( 2 |^ i > ((N-bound C) - (S-bound C)) / r & 2 |^ i > ((E-bound C) - (W-bound C)) / t ) by POWER:46;
then ( (2 |^ i) * r > (((N-bound C) - (S-bound C)) / r) * r & (2 |^ i) * t > (((E-bound C) - (W-bound C)) / t) * t ) by A1, A2, XREAL_1:70;
then ( (2 |^ i) * r > (N-bound C) - (S-bound C) & (2 |^ i) * t > (E-bound C) - (W-bound C) ) by A1, A2, XCMPLX_1:88;
then ( ((2 |^ i) * r) / (2 |^ i) > ((N-bound C) - (S-bound C)) / (2 |^ i) & ((2 |^ i) * t) / (2 |^ i) > ((E-bound C) - (W-bound C)) / (2 |^ i) ) by A7, XREAL_1:76;
then A9: ( ((N-bound C) - (S-bound C)) / (2 |^ i) < r & ((E-bound C) - (W-bound C)) / (2 |^ i) < t ) by A7, XCMPLX_1:90;
A10: len (Gauge C,i) = width (Gauge C,i) by JORDAN8:def 1;
len (Gauge C,i) >= 4 by JORDAN8:13;
then ( 1 <= len (Gauge C,i) & 1 + 1 <= width (Gauge C,i) ) by A10, XXREAL_0:2;
then ( [1,1] in Indices (Gauge C,i) & [1,(1 + 1)] in Indices (Gauge C,i) & [(1 + 1),1] in Indices (Gauge C,i) ) by A10, 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 A9, Th19, Th20; :: thesis: verum