let i, n, j, m be Element of NAT ; :: thesis: for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge E,n) & 1 <= j & j <= len (Gauge E,m) & m <= n holds
((Gauge E,n) * (len (Gauge E,n)),i) `1 <= ((Gauge E,m) * (len (Gauge E,m)),j) `1
let E be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( 1 <= i & i <= len (Gauge E,n) & 1 <= j & j <= len (Gauge E,m) & m <= n implies ((Gauge E,n) * (len (Gauge E,n)),i) `1 <= ((Gauge E,m) * (len (Gauge E,m)),j) `1 )
set w = W-bound E;
set e = E-bound E;
set G = Gauge E,n;
set M = Gauge E,m;
assume that
A1: ( 1 <= i & i <= len (Gauge E,n) ) and
A2: ( 1 <= j & j <= len (Gauge E,m) ) and
A3: m <= n ; :: thesis: ((Gauge E,n) * (len (Gauge E,n)),i) `1 <= ((Gauge E,m) * (len (Gauge E,m)),j) `1
A4: len (Gauge E,m) = width (Gauge E,m) by JORDAN8:def 1;
1 <= len (Gauge E,m) by A2, XXREAL_0:2;
then [(len (Gauge E,m)),j] in Indices (Gauge E,m) by A2, A4, MATRIX_1:37;
then A5: ((Gauge E,m) * (len (Gauge E,m)),j) `1 = (E-bound E) + (((E-bound E) - (W-bound E)) / (2 |^ m)) by Lm14;
A6: len (Gauge E,n) = width (Gauge E,n) by JORDAN8:def 1;
1 <= len (Gauge E,n) by A1, XXREAL_0:2;
then [(len (Gauge E,n)),i] in Indices (Gauge E,n) by A1, A6, MATRIX_1:37;
then ( 0 < (E-bound E) - (W-bound E) & ((Gauge E,n) * (len (Gauge E,n)),i) `1 = (E-bound E) + (((E-bound E) - (W-bound E)) / (2 |^ n)) ) by Lm14, SPRECT_1:33, XREAL_1:52;
hence ((Gauge E,n) * (len (Gauge E,n)),i) `1 <= ((Gauge E,m) * (len (Gauge E,m)),j) `1 by A3, A5, Lm8; :: thesis: verum