for d being non zero Nat
for G being Grating of d
for C being Cycle of d,G holds C ` is Cycle of d,G