let k be Element of NAT ; :: thesis: for d being non zero Element of NAT
for G being Grating of d
for C being Chain of (k + 1),G holds
( C is Cycle of k + 1,G iff del C = 0_ k,G )
let d be non zero Element of NAT ; :: thesis: for G being Grating of d
for C being Chain of (k + 1),G holds
( C is Cycle of k + 1,G iff del C = 0_ k,G )
let G be Grating of d; :: thesis: for C being Chain of (k + 1),G holds
( C is Cycle of k + 1,G iff del C = 0_ k,G )
let C be Chain of (k + 1),G; :: thesis: ( C is Cycle of k + 1,G iff del C = 0_ k,G )

hereby :: thesis: ( del C = 0_ k,G implies C is Cycle of k + 1,G )

assume C is Cycle of k + 1,G ; :: thesis: del C = 0_ k,G
then ex k' being Element of NAT st
( k + 1 = k' + 1 & ex C' being Chain of (k' + 1),G st
( C' = C & del C' = 0_ k',G ) ) by Def15;
hence del C = 0_ k,G ; :: thesis: verum

end;

thus ( del C = 0_ k,G implies C is Cycle of k + 1,G ) by Def15; :: thesis: verum