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 )

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 )

thus
( card C is even implies C is Cycle of 0 ,G )
by Def14; :: thesis: verumassume
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;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