theorem Th154: :: GLCOLO00:154

for V being set
for G2 being _Graph
for G1 being addVertices of G2,V
for t1 being TColoring of G1
for t2 being TColoring of G2
for h being Function st dom h = V \ (the_Vertices_of G2) & t1 _V = (t2 _V) +* h & t1 _E = t2 _E & t2 is proper holds
t1 is proper