theorem :: GLCOLO00:197

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