take the edgeless _Graph ; :: thesis: the edgeless _Graph is finite-tcolorable
thus the edgeless _Graph is finite-tcolorable ; :: thesis: verum