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