theorem Th149: :: GLCOLO00:149
for G being _Graph
for f being VColoring of G
for g being EColoring of G st g is proper holds
ex g9 being proper EColoring of G st
( rng f misses rng g9 & card (rng g) = card (rng g9) )