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) )

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 )

thus
( del C = 0_ (k,G) implies C is Cycle of k + 1,G )
by Def14; :: thesis: verumassume
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;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