let i, j, m, n be Nat; 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)) * (i,(len (Gauge (E,n))))) `2 <= ((Gauge (E,m)) * (j,(len (Gauge (E,m))))) `2
let E be compact non horizontal non vertical Subset of (TOP-REAL 2); ( 1 <= i & i <= len (Gauge (E,n)) & 1 <= j & j <= len (Gauge (E,m)) & m <= n implies ((Gauge (E,n)) * (i,(len (Gauge (E,n))))) `2 <= ((Gauge (E,m)) * (j,(len (Gauge (E,m))))) `2 )
set a = N-bound E;
set s = S-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
; ((Gauge (E,n)) * (i,(len (Gauge (E,n))))) `2 <= ((Gauge (E,m)) * (j,(len (Gauge (E,m))))) `2
A4:
len (Gauge (E,m)) = width (Gauge (E,m))
by JORDAN8:def 1;
1 <= len (Gauge (E,m))
by A2, XXREAL_0:2;
then
[j,(len (Gauge (E,m)))] in Indices (Gauge (E,m))
by A2, A4, MATRIX_0:30;
then A5:
((Gauge (E,m)) * (j,(len (Gauge (E,m))))) `2 = (N-bound E) + (((N-bound E) - (S-bound E)) / (2 |^ m))
by Lm13;
A6:
len (Gauge (E,n)) = width (Gauge (E,n))
by JORDAN8:def 1;
1 <= len (Gauge (E,n))
by A1, XXREAL_0:2;
then
[i,(len (Gauge (E,n)))] in Indices (Gauge (E,n))
by A1, A6, MATRIX_0:30;
then
( 0 < (N-bound E) - (S-bound E) & ((Gauge (E,n)) * (i,(len (Gauge (E,n))))) `2 = (N-bound E) + (((N-bound E) - (S-bound E)) / (2 |^ n)) )
by Lm13, SPRECT_1:32, XREAL_1:50;
hence
((Gauge (E,n)) * (i,(len (Gauge (E,n))))) `2 <= ((Gauge (E,m)) * (j,(len (Gauge (E,m))))) `2
by A3, A5, Lm8; verum