theorem :: GLCOLO00:204

for V being set
for G2 being _Graph
for v being object
for G1 being addAdjVertexAll of G2,v,V holds G1 .tChromaticNum() c= ((G2 .tChromaticNum()) +` 1) +` (card V)