per cases
( k = 0 or ex k9 being Nat st k = k9 + 1 )
by NAT_1:6;

end;

suppose A1:
k = 0
; :: thesis: ex b_{1} being Chain of k,G st

( ( k = 0 & card b_{1} is even ) or ex k9 being Nat st

( k = k9 + 1 & ex C being Chain of (k9 + 1),G st

( C = b_{1} & del C = 0_ (k9,G) ) ) )

( ( k = 0 & card b

( k = k9 + 1 & ex C being Chain of (k9 + 1),G st

( C = b

take
0_ (k,G)
; :: thesis: ( ( 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) ) ) )

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: verum

end;( k = k9 + 1 & ex C being Chain of (k9 + 1),G st

( C = 0_ (k,G) & del C = 0_ (k9,G) ) ) )

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: verum

suppose
ex k9 being Nat st k = k9 + 1
; :: thesis: ex b_{1} being Chain of k,G st

( ( k = 0 & card b_{1} is even ) or ex k9 being Nat st

( k = k9 + 1 & ex C being Chain of (k9 + 1),G st

( C = b_{1} & del C = 0_ (k9,G) ) ) )

( ( k = 0 & card b

( k = k9 + 1 & ex C being Chain of (k9 + 1),G st

( C = b

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: ( ( 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) ) ) )

( k = k9 + 1 & ex C being Chain of (k9 + 1),G st

( C = C9 & del C = 0_ (k9,G) ) ) ) ; :: thesis: verum

end;A2: k = k9 + 1 ;

reconsider k9 = k9 as Element of NAT by ORDINAL1:def 12;

take C9 = 0_ (k,G); :: thesis: ( ( 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) ) ) )

now :: thesis: ex k9 being Element of NAT st

( k = k9 + 1 & ex C being Chain of (k9 + 1),G st

( C = C9 & del C = 0_ (k9,G) ) )

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) ) )

take k9 = k9; :: thesis: ( k = k9 + 1 & ex C being Chain of (k9 + 1),G st

( C = C9 & del C = 0_ (k9,G) ) )

thus k = k9 + 1 by A2; :: thesis: ex C being Chain of (k9 + 1),G st

( C = C9 & del C = 0_ (k9,G) )

reconsider C = C9 as Chain of (k9 + 1),G by A2;

take C = C; :: thesis: ( C = C9 & del C = 0_ (k9,G) )

thus ( C = C9 & del C = 0_ (k9,G) ) by A2, Th56; :: thesis: verum

end;( C = C9 & del C = 0_ (k9,G) ) )

thus k = k9 + 1 by A2; :: thesis: ex C being Chain of (k9 + 1),G st

( C = C9 & del C = 0_ (k9,G) )

reconsider C = C9 as Chain of (k9 + 1),G by A2;

take C = C; :: thesis: ( C = C9 & del C = 0_ (k9,G) )

thus ( C = C9 & del C = 0_ (k9,G) ) by A2, Th56; :: thesis: verum

( k = k9 + 1 & ex C being Chain of (k9 + 1),G st

( C = C9 & del C = 0_ (k9,G) ) ) ) ; :: thesis: verum