theorem Th3: :: GLCOLO00:3

for G being _Graph
for f being VColoring of G
for H being Subgraph of G holds f | (the_Vertices_of H) is VColoring of H