let R be finite RelStr ; :: thesis: chromatic# R <= card the carrier of R
consider C being finite Coloring of R such that
A: card C = chromatic# R by Lchro;
card C c= card the carrier of R by Partcard;
hence chromatic# R <= card the carrier of R by A, NAT_1:40; :: thesis: verum