let G be _Graph; :: thesis: ( G is loopless & G is c -vertex implies G is c -vcolorable )
assume A1: ( G is loopless & G is c -vertex ) ; :: thesis: G is c -vcolorable
reconsider f = id (the_Vertices_of G) as VColoring of G ;
card (rng f) = G .order()
.= c by A1, GLIB_013:def 3 ;
hence G is c -vcolorable by A1; :: thesis: verum