theorem Th78: :: GLCOLO00:78

for G being _Graph
for g being EColoring of G
for H being Subgraph of G holds g | (the_Edges_of H) is EColoring of H