theorem Th96: :: GLCOLO00:96

for G2 being _Graph
for v being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for g2 being EColoring of G2
for g1 being EColoring of G1
for X, E being set st E = G1 .edgesBetween (V,{v}) & rng g2 c= X & g1 = g2 +* <:(E --> X),(id E):> & not v in the_Vertices_of G2 & g2 is proper holds
g1 is proper