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