theorem Th57: :: CHAIN_1:60

for d9 being Nat
for G being Grating of d9 + 1 holds del (Omega G) = 0_ (d9,G)