theorem :: CHAIN_1:68

for k being Nat
for d being non zero Nat
for G being Grating of d
for x being set holds
( x is Chain of k,G iff x is GrChain of k,G ) by Def16;