consider C being finite Coloring of R such that
A1: card C = chromatic# R by Def3;
C is empty ;
hence chromatic# R is empty by A1; :: thesis: verum