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

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

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

end;

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

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

end;

end;