consider C being finite Clique of R such that
A1: for D being finite Clique of R holds card D <= card C by Def3;
set sS = subrelstr S;
defpred S₁[ Nat] means ex c being finite Clique of (subrelstr S) st card c = R;
A2: for k being Nat st S₁[k] holds
k <= card C

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= card C )
assume S₁[k] ; :: thesis: k <= card C
then consider c being finite Clique of (subrelstr S) such that
A3: card c = k ;
c is finite Clique of R by Th28;
hence k <= card C by A3, A1; :: thesis: verum

end;

card ({} (subrelstr S)) = 0 ;
then A4: ex k being Nat st S₁[k] ;
consider k being Nat such that
A5: S₁[k] and
A6: for n being Nat st S₁[n] holds
n <= k from NAT_1:sch 6(A2, A4);
consider c being finite Clique of (subrelstr S) such that
A7: card c = k by A5;
for D being finite Clique of (subrelstr S) holds card D <= card c by A7, A6;
hence subrelstr S is with_finite_clique# ; :: thesis: verum