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;
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 ;
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