let G1 be _Graph; :: thesis: for G2 being loopless _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
G1 .vChromaticNum() c= G2 .vChromaticNum()
let G2 be loopless _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
G1 .vChromaticNum() c= G2 .vChromaticNum()
let F be PGraphMapping of G1,G2; :: thesis: ( F is weak_SG-embedding implies G1 .vChromaticNum() c= G2 .vChromaticNum() )
assume F is weak_SG-embedding ; :: thesis: G1 .vChromaticNum() c= G2 .vChromaticNum()
then G1 is G2 .vChromaticNum() -vcolorable by Th42, Th54;
hence G1 .vChromaticNum() c= G2 .vChromaticNum() by Th57; :: thesis: verum