for d9 being Nat
for d being non zero Nat
for G being Grating of d st d = d9 + 1 holds
for A being Cell of d9,G holds card (star A) = 2