let R be finite RelStr ; :: thesis: chromatic# R <= card the carrier of R
consider C being finite Coloring of R such that
A1: card C = chromatic# R by Def3;
Segm (card C) c= Segm (card the carrier of R) by Th7;
hence chromatic# R <= card the carrier of R by A1, NAT_1:39; :: thesis: verum