per cases ( k = 0 or ex k' being Nat st k = k' + 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

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 Th56;
hence del {B} is Cycle of 0 ,G by Def15; :: 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 ( C1 c= C & C2 c= C & S₁[C1] & S₁[C2] ) ; :: thesis: S₁[C1 + C2]
then reconsider C1' = del C1, C2' = del C2 as Cycle of k,G ;
del (C1 + C2) = C1' + C2' by Th63;
hence S₁[C1 + C2] ; :: thesis: verum

end;

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

end;

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

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

end;

end;