let G be _Graph; :: thesis: G .eChromaticNum() c= G .size()
( G is G .size() -ecolorable & G .size() c= G .size() ) by Th100;
then G .size() in H₂(G) ;
hence G .eChromaticNum() c= G .size() by SETFAM_1:3; :: thesis: verum