set sS = subrelstr S;
consider C being Clique-partition of R such that
A: C is finite by Lwfcc;
B: the carrier of (subrelstr S) = S by YELLOW_0:def 15;
reconsider CS = C | S as a_partition of S ;
for x being set st x in CS holds
x is Clique of (subrelstr S)

proof

let x be set ; :: thesis: ( x in CS implies x is Clique of (subrelstr S) )
assume x in CS ; :: thesis: x is Clique of (subrelstr S)
then consider X being Element of C such that
A1: x = X /\ S and
B1: X meets S ;
ex y being set st
( y in X & y in S ) by B1, XBOOLE_0:3;
then X is Clique of R by DILWORTH:def 11;
hence x is Clique of (subrelstr S) by A1, DILWORTH:29; :: thesis: verum

end;

then CS is Clique-partition of (subrelstr S) by B, DILWORTH:def 11;
hence subrelstr S is with_finite_cliquecover# by A, Lwfcc; :: thesis: verum