theorem Th40:
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