let G be _Graph; :: thesis: for c being Cardinal holds
( ( G is c -ecolorable & ( for d being Cardinal st G is d -ecolorable holds
c c= d ) ) iff G .eChromaticNum() = c )
let c be Cardinal; :: thesis: ( ( G is c -ecolorable & ( for d being Cardinal st G is d -ecolorable holds
c c= d ) ) iff G .eChromaticNum() = c )
( G is G .size() -ecolorable & G .size() c= G .size() ) by Th100;
then A1: G .size() in H₂(G) ;

hereby :: thesis: ( G .eChromaticNum() = c implies ( G is c -ecolorable & ( for d being Cardinal st G is d -ecolorable holds
c c= d ) ) )

assume G is c -ecolorable ; :: thesis: ( ( for d being Cardinal st G is d -ecolorable holds
c c= d ) implies G .eChromaticNum() = c )
then A2: G .eChromaticNum() c= c by Lm15;
assume A3: for d being Cardinal st G is d -ecolorable holds
c c= d ; :: thesis: G .eChromaticNum() = c

now :: thesis: for x being set st x in H₂(G) holds
c c= x

let x be set ; :: thesis: ( x in H₂(G) implies c c= x )
assume x in H₂(G) ; :: thesis: c c= x
then consider d being cardinal Subset of (G .size()) such that
A4: ( x = d & G is d -ecolorable ) ;
thus c c= x by A3, A4; :: thesis: verum

end;

then c c= G .eChromaticNum() by A1, SETFAM_1:5;
hence G .eChromaticNum() = c by A2, XBOOLE_0:def 10; :: thesis: verum

end;

thus ( G .eChromaticNum() = c implies ( G is c -ecolorable & ( for d being Cardinal st G is d -ecolorable holds
c c= d ) ) ) by Lm14, Lm15; :: thesis: verum