consider n being Nat such that
A1: G is n -tcolorable by Def12;
G .tChromaticNum() c= n by A1, Th189;
hence G .tChromaticNum() is natural ; :: thesis: verum