consider d9 being Nat such that
A1: d = d9 + 1 by NAT_1:6;
reconsider d9 = d9 as Element of NAT by ORDINAL1:def 12;
reconsider G = G as Grating of d9 + 1 by A1;
del (Omega G) = 0_ (d9,G) by Th57;
hence Omega G is Cycle of d,G by A1, Def14; :: thesis: verum