let n be Nat; :: thesis: chromatic# (CompleteRelStr n) = n
set R = CompleteRelStr n;
clique# (CompleteRelStr n) = n by CompleteCli;
then B: n <= chromatic# (CompleteRelStr n) by CliChr;
C: chromatic# (CompleteRelStr n) <= card the carrier of (CompleteRelStr n) by Maxchromatic;
card (card n) = card n ;
then card n = n by CARD_1:71;
then card the carrier of (CompleteRelStr n) = n by LNRS;
hence chromatic# (CompleteRelStr n) = n by B, C, XXREAL_0:1; :: thesis: verum