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