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