set sS = subrelstr S;
consider C being Clique-partition of R such that
A1: C is finite by Def4;
A2: 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
A3: x = X /\ S and
A4: X meets S ;
ex y being object st
( y in X & y in S ) by A4, XBOOLE_0:3;
then X is Clique of R by DILWORTH:def 11;
hence x is Clique of (subrelstr S) by A3, DILWORTH:29; :: thesis: verum

end;

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