let R be symmetric with_finite_cliquecover# RelStr ; :: thesis: cliquecover# R = chromatic# (ComplRelStr R)
set CR = ComplRelStr R;
set k = chromatic# (ComplRelStr R);
consider C being finite Coloring of (ComplRelStr R) such that
A1: card C = chromatic# (ComplRelStr R) by Def3;
C is Clique-partition of R by Th28;
then A2: ex C being finite Clique-partition of R st card C = chromatic# (ComplRelStr R) by A1;
now :: thesis: for C being finite Clique-partition of R holds not chromatic# (ComplRelStr R) > card C
let C be finite Clique-partition of R; :: thesis: not chromatic# (ComplRelStr R) > card C
assume A3: chromatic# (ComplRelStr R) > card C ; :: thesis: contradiction
C is Coloring of (ComplRelStr R) by Th27;
hence contradiction by A3, Def3; :: thesis: verum
end;
hence cliquecover# R = chromatic# (ComplRelStr R) by A2, Def5; :: thesis: verum