theorem :: JORDAN8:12

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