theorem Th70: :: GLCOLO00:70

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