theorem Th147: :: GLCOLO00:147

for G being _Graph
for t being TColoring of G st t _V is proper & t _E is proper & rng (t _V) misses rng (t _E) holds
t is proper