theorem Th24: :: GLCOLO00:24

for G2 being _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w
for f1 being VColoring of G1
for f2 being VColoring of G2
for x being object st not w in the_Vertices_of G2 & f1 = f2 +* (w .--> x) & x <> f2 . v & f2 is proper holds
f1 is proper