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