defpred
S
_{1}
[
Cell
of
k
,
G
]
means
(
k
+
1
<=
d
&
card
(
(
star
$1
)
/\
C
)
is
odd
);
{
A
where
A
is
Cell
of
k
,
G
:
S
_{1}
[
A
] }
c=
cells
(
k
,
G
)
from
FRAENKEL:sch 10
();
hence
{
A
where
A
is
Cell
of
k
,
G
: (
k
+
1
<=
d
&
card
(
(
star
A
)
/\
C
)
is
odd
) } is
Chain
of
k
,
G
;
:: thesis:
verum