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

suppose A1: k = 0 ; :: thesis: 0_ k,G is Cycle of k,G

( {} = 0_ k,G & card {} = 2 * 0 ) ;
hence 0_ k,G is Cycle of k,G by A1, Def15; :: thesis: verum

end;

suppose ex k' being Nat st k = k' + 1 ; :: thesis: 0_ k,G is Cycle of k,G

then consider k' being Nat such that
A2: k = k' + 1 ;
reconsider k' = k' as Element of NAT by ORDINAL1:def 13;
del (0_ (k' + 1),G) = 0_ k',G by Th61;
hence 0_ k,G is Cycle of k,G by A2, Def15; :: thesis: verum

end;

end;