let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies G1 .eChromaticNum() = G2 .eChromaticNum() )
assume A1: G1 == G2 ; :: thesis: G1 .eChromaticNum() = G2 .eChromaticNum()
then A2: G2 is G1 .eChromaticNum() -ecolorable by Lm14, Th103;
for c being Cardinal st G2 is c -ecolorable holds
G1 .eChromaticNum() c= c by A1, Th103, Lm15;
hence G1 .eChromaticNum() = G2 .eChromaticNum() by A2, Th122; :: thesis: verum