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