theorem Th47: :: CHAIN_1:50

for k being Nat
for d being non zero Nat
for G being Grating of d
for A being Cell of k,G
for B being Cell of (k + 1),G holds
( B in star A iff A c= B )