theorem Th123: :: GLCOLO00:123

for G being loopless _Graph holds G .supDegree() c= G .eChromaticNum()