let n be non zero Nat; :: thesis:
set R = CompleteRelStr n;
set cR = the carrier of (CompleteRelStr n);
reconsider C = { the carrier of (CompleteRelStr n)} as a_partition of the carrier of (CompleteRelStr n) by EQREL_1:39;

A1: now :: thesis:

let x be set ; :: thesis:
assume x in C ; :: thesis:
then x = [#] (CompleteRelStr n) by TARSKI:def 1;
hence x is Clique of (CompleteRelStr n) ; :: thesis:

end;

A2: now :: thesis:

take C = C; :: thesis:
thus C is finite ; :: thesis:
thus C is Clique-partition of (CompleteRelStr n) by A1, DILWORTH:def 11; :: thesis:
thus card C = 1 by CARD_1:30; :: thesis:

end;

now :: thesis:

let C be finite Clique-partition of (CompleteRelStr n); :: thesis:
0 + 1 <= card C by NAT_1:13;
hence 1 <= card C ; :: thesis:

end;

hence cliquecover# (CompleteRelStr n) = 1 by A2, Def5; :: thesis: