consider C being finite Clique of R such that
A: for D being finite Clique of R holds card D <= card C by Lfheight;
set sS = subrelstr S;
defpred S₁[ Nat] means ex c being finite Clique of (subrelstr S) st card c = R;
P1: 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
A1: card c = k ;
c is finite Clique of R by SPClique;
hence k <= card C by A1, A; :: thesis: verum

end;

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