consider n being Nat such that
A1: G is n -vcolorable by Def3;
G .vChromaticNum() c= n by A1, Th57;
hence G .vChromaticNum() is natural ; :: thesis: verum