defpred S₁[ set , set , set ] means ( ( $2 is MCS:Labeling of G & $1 is Nat & ex nn being Nat ex Gn, Gn1 being MCS:Labeling of G st
( $1 = nn & $2 = Gn & $3 = Gn1 & Gn1 = MCS:Step Gn ) ) or ( ( not $2 is MCS:Labeling of G or not $1 is Nat ) & $2 = $3 ) );

now :: thesis: for n, x being set ex y being set st S₁[n,x,y]

let n, x be set ; :: thesis: ex y being set st S₁[n,x,y]

now :: thesis: ex y being set st S₁[n,x,y]

per cases ( ( x is MCS:Labeling of G & n is Nat ) or not x is MCS:Labeling of G or not n is Nat ) ;

suppose A1: ( x is MCS:Labeling of G & n is Nat ) ; :: thesis: ex y being set st S₁[n,x,y]

then reconsider Gn = x as MCS:Labeling of G ;
ex SGn being MCS:Labeling of G st SGn = MCS:Step Gn ;
hence ex y being set st S₁[n,x,y] by A1; :: thesis: verum

end;

suppose ( not x is MCS:Labeling of G or not n is Nat ) ; :: thesis: ex y being set st S₁[n,x,y]

hence ex y being set st S₁[n,x,y] ; :: thesis: verum

end;

end;

end;

hence ex y being set st S₁[n,x,y] ; :: thesis: verum

end;

then A2: for n being Nat
for x being set ex y being set st S₁[n,x,y] ;
consider IT being Function such that
A3: ( dom IT = NAT & IT . 0 = MCS:Init G & ( for n being Nat holds S₁[n,IT . n,IT . (n + 1)] ) ) from RECDEF_1:sch 1(A2);
reconsider IT = IT as ManySortedSet of NAT by A3, PARTFUN1:def 2, RELAT_1:def 18;
defpred S₂[ Nat] means IT . $1 is MCS:Labeling of G;

A4: now :: thesis: for n being Nat st S₂[n] holds
S₂[n + 1]

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A5: S₂[n] ; :: thesis: S₂[n + 1]
ex nn being Nat ex Gn, Gn1 being MCS:Labeling of G st
( n = nn & IT . n = Gn & IT . (n + 1) = Gn1 & Gn1 = MCS:Step Gn ) by A3, A5;
hence S₂[n + 1] ; :: thesis: verum

end;

A6: S₂[ 0 ] by A3;
for n being Nat holds S₂[n] from NAT_1:sch 2(A6, A4);
then reconsider IT = IT as MCS:LabelingSeq of G by Def23;
take IT ; :: thesis: ( IT . 0 = MCS:Init G & ( for n being Nat holds IT . (n + 1) = MCS:Step (IT . n) ) )
thus IT . 0 = MCS:Init G by A3; :: thesis: for n being Nat holds IT . (n + 1) = MCS:Step (IT . n)
let n be Nat; :: thesis: IT . (n + 1) = MCS:Step (IT . n)
ex nn being Nat ex Gn, Gn1 being MCS:Labeling of G st
( n = nn & IT . n = Gn & IT . (n + 1) = Gn1 & Gn1 = MCS:Step Gn ) by A3;
hence IT . (n + 1) = MCS:Step (IT . n) ; :: thesis: verum