theorem Th89: :: GLCOLO00:89

for G being _Graph
for g being EColoring of G
for H being Subgraph of G
for g9 being EColoring of H st g9 = g | (the_Edges_of H) & g is proper holds
g9 is proper