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