let k be Nat; :: thesis: for d being non zero 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 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 k9 being Nat st
( k + 1 = k9 + 1 & ex C9 being Chain of (k9 + 1),G st
( C9 = C & del C9 = 0_ (k9,G) ) ) by Def14;
hence del C = 0_ (k,G) ; :: thesis: verum

end;

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