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