theorem :: GLCOLO00:164

for G being _Graph
for f being VColoring of G
for t being TColoring of G st G is edgeless & f is proper & t = [f,{}] holds
t is proper ;