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