theorem :: JORDAN8:14

for i, n being Nat
for T being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (T,n)) holds
((Gauge (T,n)) * (i,((len (Gauge (T,n))) -' 1))) `2 = N-bound T