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
Aa: card C = chromatic# (ComplRelStr R) by Lchro;
C is Clique-partition of R by ChrComplClico;
then A: ex C being finite Clique-partition of R st card C = chromatic# (ComplRelStr R) by Aa;

now

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

end;

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