let i, j, k, m be 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,(j + 1)] in Indices (Gauge (C,k)) holds
dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1))))
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( m > k & [i,j] in Indices (Gauge (C,k)) & [i,(j + 1)] in Indices (Gauge (C,k)) implies dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1)))) )
assume that
A1: m > k and
A2: [i,j] in Indices (Gauge (C,k)) and
A3: [i,(j + 1)] in Indices (Gauge (C,k)) ; :: thesis: dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1))))
A4: len (Gauge (C,k)) < len (Gauge (C,m)) by A1, JORDAN1A:29;
A5: len (Gauge (C,m)) = width (Gauge (C,m)) by JORDAN8:def 1;
A6: len (Gauge (C,k)) = width (Gauge (C,k)) by JORDAN8:def 1;
j <= width (Gauge (C,k)) by A2, MATRIX_0:32;
then A7: j <= width (Gauge (C,m)) by A6, A5, A4, XXREAL_0:2;
A8: (N-bound C) - (S-bound C) > 0 by SPRECT_1:32, XREAL_1:50;
i <= len (Gauge (C,k)) by A2, MATRIX_0:32;
then A9: i <= len (Gauge (C,m)) by A4, XXREAL_0:2;
j + 1 <= width (Gauge (C,k)) by A3, MATRIX_0:32;
then A10: j + 1 <= width (Gauge (C,m)) by A6, A5, A4, XXREAL_0:2;
A11: 1 <= i by A2, MATRIX_0:32;
1 <= j + 1 by NAT_1:11;
then A12: [i,(j + 1)] in Indices (Gauge (C,m)) by A11, A9, A10, MATRIX_0:30;
1 <= j by A2, MATRIX_0:32;
then [i,j] in Indices (Gauge (C,m)) by A11, A9, A7, MATRIX_0:30;
then A13: dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ m) by A12, GOBRD14:9;
A14: 2 |^ k > 0 by NEWTON:83;
dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ k) by A2, A3, GOBRD14:9;
hence dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1)))) by A1, A13, A14, A8, PEPIN:66, XREAL_1:76; :: thesis: verum