theorem Th160: :: GLCOLO00:160

for G, G1 being _Graph
for t being TColoring of G
for F being PGraphMapping of G1,G
for t9 being TColoring of G1 st F is weak_SG-embedding & t9 = [((t _V) * (F _V)),((t _E) * (F _E))] & t is proper holds
t9 is proper