theorem :: GLCOLO00:205

for G1 being _Graph
for G2 being loopless _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
G1 .tChromaticNum() c= G2 .tChromaticNum()