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

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