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 + 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:29;
i <= len (Gauge (C,k)) by A2, MATRIX_0:32;
then A5: i <= len (Gauge (C,m)) by A4, XXREAL_0:2;
A6: (E-bound C) - (W-bound C) > 0 by SPRECT_1:31, XREAL_1:50;
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_0:32;
then A9: j <= width (Gauge (C,m)) by A8, A7, A4, XXREAL_0:2;
i + 1 <= len (Gauge (C,k)) by A3, MATRIX_0:32;
then A10: i + 1 <= len (Gauge (C,m)) by A4, XXREAL_0:2;
A11: 1 <= j by A2, MATRIX_0:32;
1 <= i + 1 by NAT_1:11;
then A12: [(i + 1),j] in Indices (Gauge (C,m)) by A11, A9, A10, MATRIX_0:30;
1 <= i by A2, MATRIX_0:32;
then [i,j] in Indices (Gauge (C,m)) by A11, A5, A9, MATRIX_0:30;
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:10;
A14: 2 |^ k > 0 by NEWTON:83;
dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * ((i + 1),j))) = ((E-bound C) - (W-bound C)) / (2 |^ k) by A2, A3, GOBRD14:10;
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:66, XREAL_1:76; :: thesis: verum