defpred S₁[ Nat] means ex C being finite Clique-partition of R st card C = $1;
consider C being Clique-partition of R such that
A: C is finite by Lwfcc;
card C = card C ;
then P: ex k being Nat st S₁[k] by A;
consider n being Nat such that
Q1: S₁[n] and
Q2: for k being Nat st S₁[k] holds
n <= k from NAT_1:sch 5(P);
take n ; :: thesis: ( ex C being finite Clique-partition of R st card C = n & ( for C being finite Clique-partition of R holds n <= card C ) )
thus ex C being finite Clique-partition of R st card C = n by Q1; :: thesis: for C being finite Clique-partition of R holds n <= card C
let C be finite Clique-partition of R; :: thesis: n <= card C
thus n <= card C by Q2; :: thesis: verum