theorem :: GLCOLO00:74
for G1 being _Graph
for G2 being loopless _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
G1 .vChromaticNum() c= G2 .vChromaticNum()