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