theorem
:: JORDAN8:15
for
C
being non
empty
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
for
i
,
n
being
Nat
st
i
<=
len
(
Gauge
(
C
,
n
)
)
holds
cell
(
(
Gauge
(
C
,
n
)
)
,
i
,
(
len
(
Gauge
(
C
,
n
)
)
)
)
misses
C