let G2 be _Graph; :: thesis: ( G2 is G -isomorphic implies G2 is c -ecolorable )
assume G2 is G -isomorphic ; :: thesis: G2 is c -ecolorable
then consider F being PGraphMapping of G,G2 such that
A1: F is isomorphism by GLIB_010:def 23;
thus G2 is c -ecolorable by A1, Th111; :: thesis: verum