theorem Th137: :: GLCOLO00:137
for G being _Graph
for f being VColoring of G st G is edgeless holds
[f,{}] is TColoring of G