theorem :: CHAIN_1:65

for k being Nat
for d being non zero Nat
for G being Grating of d st k > d holds
for C being Chain of k,G holds C is Cycle of k,G