consider n being Nat such that
A1: G is n -ecolorable by Def7;
G .eChromaticNum() c= n by A1, Lm15;
hence G .eChromaticNum() is natural ; :: thesis: verum