let R be symmetric with_finite_chromatic# RelStr ; :: thesis: chromatic# R = cliquecover# (ComplRelStr R)
set CR = ComplRelStr R;
set k = cliquecover# (ComplRelStr R);
consider C being finite Clique-partition of (ComplRelStr R) such that
A1: card C = cliquecover# (ComplRelStr R) by Def5;
C is Coloring of R by Th26;
then A2: ex C being finite Coloring of R st card C = cliquecover# (ComplRelStr R) by A1;

now :: thesis: for C being finite Coloring of R holds not cliquecover# (ComplRelStr R) > card C

let C be finite Coloring of R; :: thesis: not cliquecover# (ComplRelStr R) > card C
assume A3: cliquecover# (ComplRelStr R) > card C ; :: thesis: contradiction
C is Clique-partition of (ComplRelStr R) by Th25;
hence contradiction by A3, Def5; :: thesis: verum

end;

hence chromatic# R = cliquecover# (ComplRelStr R) by A2, Def3; :: thesis: verum