let k be Nat; :: thesis: for d being non zero Nat

for G being Grating of d st k > d holds

for C being Chain of k,G holds C is Cycle of k,G

let d be non zero Nat; :: thesis: for G being Grating of d st k > d holds

for C being Chain of k,G holds C is Cycle of k,G

let G be Grating of d; :: thesis: ( k > d implies for C being Chain of k,G holds C is Cycle of k,G )

assume A1: k > d ; :: thesis: for C being Chain of k,G holds C is Cycle of k,G

let C be Chain of k,G; :: thesis: C is Cycle of k,G

consider k9 being Nat such that

A2: k = k9 + 1 by A1, NAT_1:6;

reconsider k9 = k9 as Element of NAT by ORDINAL1:def 12;

reconsider C9 = C as Chain of (k9 + 1),G by A2;

del C9 = 0_ (k9,G) by A1, A2, Th49;

hence C is Cycle of k,G by A2, Def14; :: thesis: verum

for G being Grating of d st k > d holds

for C being Chain of k,G holds C is Cycle of k,G

let d be non zero Nat; :: thesis: for G being Grating of d st k > d holds

for C being Chain of k,G holds C is Cycle of k,G

let G be Grating of d; :: thesis: ( k > d implies for C being Chain of k,G holds C is Cycle of k,G )

assume A1: k > d ; :: thesis: for C being Chain of k,G holds C is Cycle of k,G

let C be Chain of k,G; :: thesis: C is Cycle of k,G

consider k9 being Nat such that

A2: k = k9 + 1 by A1, NAT_1:6;

reconsider k9 = k9 as Element of NAT by ORDINAL1:def 12;

reconsider C9 = C as Chain of (k9 + 1),G by A2;

del C9 = 0_ (k9,G) by A1, A2, Th49;

hence C is Cycle of k,G by A2, Def14; :: thesis: verum