consider C being Coloring of R such that
A: C is finite by Lwfchr;
C is Clique-partition of (ComplRelStr R) by ChrClicoCompl;
hence ComplRelStr R is with_finite_cliquecover# by A, Lwfcc; :: thesis: verum