let G be finitely_colorable SimpleGraph; :: thesis: chromatic# G = cliquecover# (Complement G)
set CG = Complement G;
set k = cliquecover# (Complement G);
consider C being finite Clique-partition of (Complement G) such that
A1: card C = cliquecover# (Complement G) by Def18;
A2: C is Coloring of G by Th78;
now :: thesis: for C being finite Coloring of G holds not cliquecover# (Complement G) > card C
let C be finite Coloring of G; :: thesis: not cliquecover# (Complement G) > card C
assume A3: cliquecover# (Complement G) > card C ; :: thesis: contradiction
C is Clique-partition of (Complement G) by Th80;
hence contradiction by A3, Def18; :: thesis: verum
end;
hence chromatic# G = cliquecover# (Complement G) by A2, A1, Def22; :: thesis: verum