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