let n be Nat; :: thesis: chromatic# (CompleteRelStr n) = n
set R = CompleteRelStr n;
clique# (CompleteRelStr n) = n by Th33;
then A1: n <= chromatic# (CompleteRelStr n) by Th15;
A2: chromatic# (CompleteRelStr n) <= card the carrier of (CompleteRelStr n) by Th13;
card n = n ;
then card the carrier of (CompleteRelStr n) = n by Def7;
hence chromatic# (CompleteRelStr n) = n by A1, A2, XXREAL_0:1; :: thesis: verum