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