let G be _Graph; :: thesis: ( G is c -tcolorable implies G is loopless )
assume G is c -tcolorable ; :: thesis: G is loopless
then G is c -vcolorable by Th162;
hence G is loopless ; :: thesis: verum