let d be non zero Nat; :: thesis: for G being Grating of d
for C being Cycle of d,G holds C ` is Cycle of d,G
let G be Grating of d; :: thesis: for C being Cycle of d,G holds C ` is Cycle of d,G
let C be Cycle of d,G; :: thesis: C ` is Cycle of d,G
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;
reconsider C = C as Cycle of d9 + 1,G by A1;
del C = 0_ (d9,G) ;
then del (C `) = 0_ (d9,G) by Th59;
hence C ` is Cycle of d,G by A1, Th61; :: thesis: verum