theorem
:: JORDAN8:7
for
i
,
j
,
k
being
Nat
for
G
being
Go-board
st
i
+
k
<
len
G
& 1
<=
j
&
j
<
width
G
&
cell
(
G
,
i
,
j
)
meets
cell
(
G
,
(
i
+
k
)
,
j
) holds
k
<=
1