defpred S₁[ Nat] means ex C being finite Coloring of G st card C = $1;
consider C being Coloring of G such that
A1: C is finite by Def21;
card C = card C ;
then A2: ex k being Nat st S₁[k] by A1;
consider n being Nat such that
A3: S₁[n] and
A4: for k being Nat st S₁[k] holds
n <= k from NAT_1:sch 5(A2);
take n ; :: thesis: ( ex C being finite Coloring of G st card C = n & ( for C being finite Coloring of G holds n <= card C ) )
thus ex C being finite Coloring of G st card C = n by A3; :: thesis: for C being finite Coloring of G holds n <= card C
let C be finite Coloring of G; :: thesis: n <= card C
thus n <= card C by A4; :: thesis: verum