let n be Nat; :: thesis: clique# (CompleteRelStr n) = n
set R = CompleteRelStr n;
Aa: card (card n) = card n ;
[#] (CompleteRelStr n) = n by LNRS;
then A: ex C being finite Clique of (CompleteRelStr n) st card C = n by Aa, CARD_1:71;
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 Aa, CARD_1:71;
then A1: card the carrier of (CompleteRelStr n) = n by LNRS;
B1: card T <= clique# (CompleteRelStr n) by DILWORTH:def 4;
clique# (CompleteRelStr n) <= n by A1, Maxclique;
hence card T <= n by B1, XXREAL_0:2; :: thesis: verum

end;

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