theorem Th150: :: GLCOLO00:150

for G being _Graph
for f being VColoring of G
for g being EColoring of G st f is proper holds
ex f9 being VColoring of G st
( f9 is proper & rng f9 misses rng g & card (rng f) = card (rng f9) )