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