let G1 be _Graph; :: thesis: for G2 being G1 -isomorphic _Graph holds G1 .eChromaticNum() = G2 .eChromaticNum()
let G2 be G1 -isomorphic _Graph; :: thesis: G1 .eChromaticNum() = G2 .eChromaticNum()
consider F being PGraphMapping of G1,G2 such that
A1: F is isomorphism by GLIB_010:def 23;
thus G1 .eChromaticNum() = G2 .eChromaticNum() by A1, Th134; :: thesis: verum