theorem :: GLCOLO00:126

for G being _Graph
for H being Subgraph of G holds H .eChromaticNum() c= G .eChromaticNum()