theorem Th25: :: GLCOLO00:25

for G2 being _Graph
for v, x being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for f1 being VColoring of G1
for f2 being VColoring of G2 st not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & not x in rng f2 & f2 is proper holds
f1 is proper