consider C being Clique-partition of G such that
A1: C is finite by Def17;
C is Coloring of (Complement G) by Th79;
hence Complement G is finitely_colorable by A1; :: thesis: verum