let G be loopless _Graph; :: thesis: for H being Subgraph of G holds H .tChromaticNum() c= G .tChromaticNum()
let H be Subgraph of G; :: thesis: H .tChromaticNum() c= G .tChromaticNum()
G is G .tChromaticNum() -tcolorable by Th186;
hence H .tChromaticNum() c= G .tChromaticNum() by Th189; :: thesis: verum