let d be non zero Nat; :: thesis: for G being Grating of d
for C being Chain of 0,G holds
( C is Cycle of 0 ,G iff card C is even )
let G be Grating of d; :: thesis: for C being Chain of 0,G holds
( C is Cycle of 0 ,G iff card C is even )
let C be Chain of 0,G; :: thesis: ( C is Cycle of 0 ,G iff card C is even )

hereby :: thesis: ( card C is even implies C is Cycle of 0 ,G )

assume C is Cycle of 0 ,G ; :: thesis: card C is even
then ( ( 0 = 0 & card C is even ) or ex k9 being Nat st
( 0 = k9 + 1 & ex C9 being Chain of (k9 + 1),G st
( C9 = C & del C9 = 0_ (k9,G) ) ) ) by Def14;
hence card C is even ; :: thesis: verum

end;

thus ( card C is even implies C is Cycle of 0 ,G ) by Def14; :: thesis: verum