let G be _Graph; :: thesis: for c being Cardinal st G is c -ecolorable holds
G .eChromaticNum() c= c
let c be Cardinal; :: thesis: ( G is c -ecolorable implies G .eChromaticNum() c= c )
assume A1: G is c -ecolorable ; :: thesis: G .eChromaticNum() c= c

per cases ( not G .size() in c or G .size() in c ) ;

suppose not G .size() in c ; :: thesis: G .eChromaticNum() c= c

then c c= G .size() by ORDINAL1:16;
then c in H₂(G) by A1;
hence G .eChromaticNum() c= c by SETFAM_1:3; :: thesis: verum

end;

suppose G .size() in c ; :: thesis: G .eChromaticNum() c= c

then G .eChromaticNum() in c by Th120, ORDINAL1:12;
hence G .eChromaticNum() c= c by ORDINAL1:def 2; :: thesis: verum

end;

end;