take the non loopless _Graph ; :: thesis: not the non loopless _Graph is finite-tcolorable
thus not the non loopless _Graph is finite-tcolorable ; :: thesis: verum