consider C being Coloring of G such that
A1: C is finite by Def21;
C is Clique-partition of (Complement G) by Th80;
hence Complement G is with_finite_cliquecover# by A1; :: thesis: verum