defpred S₁[ set ] means A c= $1;
{ B where B is Cell of (k + 1),G : S₁[B] } c= cells ((k + 1),G) from FRAENKEL:sch 10();
hence { B where B is Cell of (k + 1),G : A c= B } is Chain of (k + 1),G ; :: thesis: verum