consider C being finite Coloring of R such that
A: card C = chromatic# R by Lchro;
C is empty by EQREL_1:41;
hence chromatic# R is empty by A; :: thesis: verum