:: deftheorem Def4 defines Grating CHAIN_1:def 4 :
for d being non zero Nat
for b₂ being Function of (Seg d),(bool REAL) holds
( b₂ is Grating of d iff for i being Element of Seg d holds
( not b₂ . i is trivial & b₂ . i is finite ) );