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