theorem Th40: :: JORDAN1A:40
for i, j, m, n being 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