let n be Nat; :: thesis: clique# (CompleteRelStr n) = n
set R = CompleteRelStr n;
A1: card (card n) = card n ;
[#] (CompleteRelStr n) = n by Def7;
then A2: ex C being finite Clique of (CompleteRelStr n) st card C = n by A1, CARD_1:40;
for T being finite Clique of (CompleteRelStr n) holds card T <= n

proof

let T be finite Clique of (CompleteRelStr n); :: thesis: card T <= n
card n = n by A1, CARD_1:40;
then A3: card the carrier of (CompleteRelStr n) = n by Def7;
A4: card T <= clique# (CompleteRelStr n) by DILWORTH:def 4;
clique# (CompleteRelStr n) <= n by A3, Th11;
hence card T <= n by A4, XXREAL_0:2; :: thesis: verum

end;

hence clique# (CompleteRelStr n) = n by A2, DILWORTH:def 4; :: thesis: verum