let n be non empty Nat; :: thesis: cliquecover# (CompleteRelStr n) = 1
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

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

end;

A2: now

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

end;

now

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

end;

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