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
Aa: card C = cliquecover# (ComplRelStr R) by Lclico;
C is Coloring of R by ClicoComplChr;
then A: ex C being finite Coloring of R st card C = cliquecover# (ComplRelStr R) by Aa;

now

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

end;

hence chromatic# R = cliquecover# (ComplRelStr R) by A, Lchro; :: thesis: verum