theorem :: GLCOLO00:170

for G2 being _Graph
for c being Cardinal
for e being object
for v, w being Vertex of G2
for G1 being addEdge of G2,v,e,w st v,w are_adjacent & G2 is c -tcolorable holds
G1 is c +` 1 -tcolorable