theorem Th175: :: GLCOLO00:175

for V being set
for G2 being _Graph
for c being Cardinal
for v being object
for G1 being addAdjVertexAll of G2,v,V st G2 is c -tcolorable holds
G1 is (c +` 1) +` (card V) -tcolorable