let G be loopless _Graph; :: thesis: G .supDegree() c= G .eChromaticNum()
G is G .eChromaticNum() -ecolorable by Lm14;
then consider g being proper EColoring of G such that
A1: card (rng g) c= G .eChromaticNum() ;
set D = { (v .degree()) where v is Vertex of G : verum } ;

now :: thesis: for x being object st x in G .supDegree() holds
x in G .eChromaticNum()

let x be object ; :: thesis: ( x in G .supDegree() implies x in G .eChromaticNum() )
assume x in G .supDegree() ; :: thesis: x in G .eChromaticNum()
then x in union { (v .degree()) where v is Vertex of G : verum } by GLIB_013:def 6;
then consider d being set such that
A2: ( x in d & d in { (v .degree()) where v is Vertex of G : verum } ) by TARSKI:def 4;
consider v being Vertex of G such that
A3: d = v .degree() by A2;
card (rng (g | (v .edgesInOut()))) c= card (rng g) by RELAT_1:70, CARD_1:11;
then A4: card (rng (g | (v .edgesInOut()))) c= G .eChromaticNum() by A1, XBOOLE_1:1;
g | (v .edgesInOut()) is one-to-one by Def5;
then card (rng (g | (v .edgesInOut()))) = card (dom (g | (v .edgesInOut()))) by CARD_1:70
.= card ((dom g) /\ (v .edgesInOut())) by RELAT_1:61
.= card ((the_Edges_of G) /\ (v .edgesInOut())) by PARTFUN1:def 2
.= card (v .edgesInOut()) by XBOOLE_1:28
.= d by A3, GLIB_000:19 ;
hence x in G .eChromaticNum() by A2, A4; :: thesis: verum

end;

hence G .supDegree() c= G .eChromaticNum() by TARSKI:def 3; :: thesis: verum