theorem Th141: :: GLCOLO00:141

for G2 being _Graph
for e being object
for v, w being Vertex of G2
for G1 being addEdge of G2,v,e,w
for t being TColoring of G2
for y being object st not e in the_Edges_of G2 holds
[(t _V),((t _E) +* (e .--> y))] is TColoring of G1