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