let G be _Graph; :: thesis: ( G is vertex-finite & G is loopless implies G is finite-vcolorable )
assume A1: ( G is vertex-finite & G is loopless ) ; :: thesis: G is finite-vcolorable
then G is G .order() -vcolorable by Th29;
hence G is finite-vcolorable by A1; :: thesis: verum