theorem :: GLCOLO00:194

for G being loopless _Graph holds (G .supDegree()) +` 1 c= G .tChromaticNum()