let k be Nat; 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; 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; 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; ( C is Cycle of k + 1,G iff del C = 0_ (k,G) )
hereby ( del C = 0_ (k,G) implies C is Cycle of k + 1,G )
end;
thus
( del C = 0_ (k,G) implies C is Cycle of k + 1,G )
by Def14; verum