:: deftheorem defines star CHAIN_1:def 11 :
for d being non zero Nat
for G being Grating of d
for k being Nat
for A being Cell of k,G holds star A = { B where B is Cell of (k + 1),G : A c= B } ;