let G be loopless _Graph; :: thesis: G .eChromaticNum() c= G .tChromaticNum()
G is G .tChromaticNum() -tcolorable by Th186;
hence G .eChromaticNum() c= G .tChromaticNum() by Th162, Lm15; :: thesis: verum