theorem Th152: :: GLCOLO00:152

for G1, G2 being _Graph
for t1 being TColoring of G1
for t2 being TColoring of G2 st G1 == G2 & t1 = t2 & t1 is proper holds
t2 is proper