defpred S₂[ Nat] means ex C being finite Coloring of R st card C = $1;
consider C being Coloring of R such that
A1: C is finite by Def2;
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 R st card C = n & ( for C being finite Coloring of R holds n <= card C ) )
thus ex C being finite Coloring of R st card C = n by A3; :: thesis: for C being finite Coloring of R holds n <= card C
let C be finite Coloring of R; :: thesis: n <= card C
thus n <= card C by A4; :: thesis: verum