let G be _Graph; :: thesis: for H being Subgraph of G holds H .eChromaticNum() c= G .eChromaticNum()
let H be Subgraph of G; :: thesis: H .eChromaticNum() c= G .eChromaticNum()
G is G .eChromaticNum() -ecolorable by Lm14;
hence H .eChromaticNum() c= G .eChromaticNum() by Lm15; :: thesis: verum