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