let i, m, k, j be Element of NAT ; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge C,k) & [(i + 1),j] in Indices (Gauge C,k) holds
dist ((Gauge C,m) * i,j),((Gauge C,m) * (i + 1),j) < dist ((Gauge C,k) * i,j),((Gauge C,k) * (i + 1),j)
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( m > k & [i,j] in Indices (Gauge C,k) & [(i + 1),j] in Indices (Gauge C,k) implies dist ((Gauge C,m) * i,j),((Gauge C,m) * (i + 1),j) < dist ((Gauge C,k) * i,j),((Gauge C,k) * (i + 1),j) )
assume that
A1: m > k and
A2: [i,j] in Indices (Gauge C,k) and
A3: [(i + 1),j] in Indices (Gauge C,k) ; :: thesis: dist ((Gauge C,m) * i,j),((Gauge C,m) * (i + 1),j) < dist ((Gauge C,k) * i,j),((Gauge C,k) * (i + 1),j)
A4: len (Gauge C,k) < len (Gauge C,m) by A1, JORDAN1A:50;
i <= len (Gauge C,k) by A2, MATRIX_1:39;
then A5: i <= len (Gauge C,m) by A4, XXREAL_0:2;
A6: (E-bound C) - (W-bound C) > 0 by SPRECT_1:33, XREAL_1:52;
A7: len (Gauge C,m) = width (Gauge C,m) by JORDAN8:def 1;
A8: len (Gauge C,k) = width (Gauge C,k) by JORDAN8:def 1;
j <= width (Gauge C,k) by A2, MATRIX_1:39;
then A9: j <= width (Gauge C,m) by A8, A7, A4, XXREAL_0:2;
i + 1 <= len (Gauge C,k) by A3, MATRIX_1:39;
then A10: i + 1 <= len (Gauge C,m) by A4, XXREAL_0:2;
A11: 1 <= j by A2, MATRIX_1:39;
1 <= i + 1 by NAT_1:11;
then A12: [(i + 1),j] in Indices (Gauge C,m) by A11, A9, A10, MATRIX_1:37;
1 <= i by A2, MATRIX_1:39;
then [i,j] in Indices (Gauge C,m) by A11, A5, A9, MATRIX_1:37;
then A13: dist ((Gauge C,m) * i,j),((Gauge C,m) * (i + 1),j) = ((E-bound C) - (W-bound C)) / (2 |^ m) by A12, GOBRD14:20;
A14: 2 |^ k > 0 by NEWTON:102;
dist ((Gauge C,k) * i,j),((Gauge C,k) * (i + 1),j) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A2, A3, GOBRD14:20;
hence dist ((Gauge C,m) * i,j),((Gauge C,m) * (i + 1),j) < dist ((Gauge C,k) * i,j),((Gauge C,k) * (i + 1),j) by A1, A13, A14, A6, PEPIN:71, XREAL_1:78; :: thesis: verum