theorem Th140: :: GLCOLO00:140

for G2 being _Graph
for v, x being object
for G1 being addVertex of G2,v
for t being TColoring of G2 holds [((t _V) +* (v .--> x)),(t _E)] is TColoring of G1