theorem
:: JORDAN8:13
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
,2)
)
`2
=
S-bound
T