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

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

defpred S₁[ Chain of (k + 1),G] means del $1 is Cycle of k,G;
del (0_ ((k + 1),G)) = 0_ (k,G) ;
then A2: S₁[ 0_ ((k + 1),G)] ;

now :: thesis: for B being Cell of (0 + 1),G st B in C holds
del {B} is Cycle of 0 ,G

let B be Cell of (0 + 1),G; :: thesis: ( B in C implies del {B} is Cycle of 0 ,G )
assume B in C ; :: thesis: del {B} is Cycle of 0 ,G
card (del {B}) = 2 * 1 by Th52;
hence del {B} is Cycle of 0 ,G by Def14; :: thesis: verum

end;

then A3: for A being Cell of (k + 1),G st A in C holds
S₁[{A}] by A1;
A4: for C1, C2 being Chain of (k + 1),G st C1 c= C & C2 c= C & S₁[C1] & S₁[C2] holds
S₁[C1 + C2]

proof

let C1, C2 be Chain of (k + 1),G; :: thesis: ( C1 c= C & C2 c= C & S₁[C1] & S₁[C2] implies S₁[C1 + C2] )
assume that
C1 c= C and
C2 c= C and
A5: S₁[C1] and
A6: S₁[C2] ; :: thesis: S₁[C1 + C2]
reconsider C19 = del C1, C29 = del C2 as Cycle of k,G by A5, A6;
del (C1 + C2) = C19 + C29 by Th58;
hence S₁[C1 + C2] ; :: thesis: verum

end;

thus S₁[C] from CHAIN_1:sch 4(A2, A3, A4); :: thesis: verum

end;

suppose ex k9 being Nat st k = k9 + 1 ; :: thesis: del C is Cycle of k,G

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

end;

end;