let G be _Graph; :: thesis: ( G is _trivial implies G .eChromaticNum() = G .size() )
assume A1: G is _trivial ; :: thesis: G .eChromaticNum() = G .size()

now :: thesis: for c being Cardinal st G is c -ecolorable holds
G .size() c= c

let c be Cardinal; :: thesis: ( G is c -ecolorable implies G .size() c= c )
assume G is c -ecolorable ; :: thesis: G .size() c= c
then consider g being proper EColoring of G such that
A2: card (rng g) c= c ;
set v = the Vertex of G;
g | ( the Vertex of G .edgesInOut()) = g | (the_Edges_of G) by A1, GLIB_000:148
.= g ;
then g is one-to-one by Def5;
then card (rng g) = card (dom g) by CARD_1:70
.= G .size() by PARTFUN1:def 2 ;
hence G .size() c= c by A2; :: thesis: verum

end;

hence G .eChromaticNum() = G .size() by Th100, Th122; :: thesis: verum