let G be loopless _Graph; :: thesis: for H being Subgraph of G holds H .vChromaticNum() c= G .vChromaticNum()
let H be Subgraph of G; :: thesis: H .vChromaticNum() c= G .vChromaticNum()
G is G .vChromaticNum() -vcolorable by Th54;
hence H .vChromaticNum() c= G .vChromaticNum() by Th57; :: thesis: verum