theorem Th171: :: GLCOLO00:171

for G2 being _Graph
for c being Cardinal
for v, e, w being object
for G1 being addEdge of G2,v,e,w st v <> w & G2 is c -tcolorable holds
G1 is c +` 2 -tcolorable