per cases by NAT_1:6;

suppose A1: k = 0 ; :: thesis:

take 0_ (k,G) ; :: thesis:
thus ( ( k = 0 & card (0_ (k,G)) is even ) or ex k9 being Nat st
( k = k9 + 1 & ex C being Chain of (k9 + 1),G st
( C = 0_ (k,G) & del C = 0_ (k9,G) ) ) ) by A1; :: thesis:

end;

suppose ex k9 being Nat st k = k9 + 1 ; :: thesis:

then consider k9 being Nat such that
A2: k = k9 + 1 ;
reconsider k9 = k9 as Element of NAT by ORDINAL1:def 12;
take C9 = 0_ (k,G); :: thesis:

now :: thesis:

take k9 = k9; :: thesis:
thus k = k9 + 1 by A2; :: thesis:
reconsider C = C9 as Chain of (k9 + 1),G by A2;
take C = C; :: thesis:
thus ( C = C9 & del C = 0_ (k9,G) ) by A2, Th56; :: thesis:

end;

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

end;

end;