let G be _Graph; :: thesis: ( G is edgeless implies G is finite-tcolorable )
assume G is edgeless ; :: thesis: G is finite-tcolorable
then G is 1 -tcolorable ;
hence G is finite-tcolorable ; :: thesis: verum