theorem Th16: :: GLCOLO00:16

for G1, G2 being _Graph
for f1 being VColoring of G1
for f2 being VColoring of G2 st G1 == G2 & f1 = f2 & f1 is proper holds
f2 is proper