let k be Element of NAT ; :: thesis: for d being non zero Element of 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 Element of 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 k' being Nat such that
A2: k = k' + 1 by A1, NAT_1:6;
reconsider k' = k' as Element of NAT by ORDINAL1:def 13;
reconsider C' = C as Chain of (k' + 1),G by A2;
( C' = C & del C' = 0_ k',G ) by A1, A2, Th53;
hence C is Cycle of k,G by A2, Def15; :: thesis: verum