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