theorem Th90: :: GLCOLO00:90

for G1, G2 being _Graph
for g1 being EColoring of G1
for g2 being EColoring of G2 st G1 == G2 & g1 = g2 & g1 is proper holds
g2 is proper