let d be non zero Element of 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 k' being Element of NAT st
( 0 = k' + 1 & ex C' being Chain of (k' + 1),G st
( C' = C & del C' = 0_ k',G ) ) ) by Def15;
hence card C is even ; :: thesis: verum

end;

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