theorem
:: JORDAN8:11
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
)
)
*
(2,
j
)
)
`1
=
W-bound
T