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