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

end;

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

defpred S_{1}[ Chain of (k + 1),G] means del $1 is Cycle of k,G;

del (0_ ((k + 1),G)) = 0_ (k,G) ;

then A2: S_{1}[ 0_ ((k + 1),G)]
;

S_{1}[{A}]
by A1;

A4: for C1, C2 being Chain of (k + 1),G st C1 c= C & C2 c= C & S_{1}[C1] & S_{1}[C2] holds

S_{1}[C1 + C2]
_{1}[C]
from CHAIN_1:sch 4(A2, A3, A4); :: thesis: verum

end;del (0_ ((k + 1),G)) = 0_ (k,G) ;

then A2: S

now :: thesis: for B being Cell of (0 + 1),G st B in C holds

del {B} is Cycle of 0 ,G

then A3:
for A being Cell of (k + 1),G st A 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;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

S

A4: for C1, C2 being Chain of (k + 1),G st C1 c= C & C2 c= C & S

S

proof

thus
S
let C1, C2 be Chain of (k + 1),G; :: thesis: ( C1 c= C & C2 c= C & S_{1}[C1] & S_{1}[C2] implies S_{1}[C1 + C2] )

assume that

C1 c= C and

C2 c= C and

A5: S_{1}[C1]
and

A6: S_{1}[C2]
; :: thesis: S_{1}[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_{1}[C1 + C2]
; :: thesis: verum

end;assume that

C1 c= C and

C2 c= C and

A5: S

A6: S

reconsider C19 = del C1, C29 = del C2 as Cycle of k,G by A5, A6;

del (C1 + C2) = C19 + C29 by Th58;

hence S

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