consider C being Coloring of R such that
A1: C is finite by Def2;
C is Clique-partition of (ComplRelStr R) by Th25;
hence ComplRelStr R is with_finite_cliquecover# by A1; :: thesis: verum