take the edgeless _Graph ; :: thesis: the edgeless _Graph is c -tcolorable
1 c= c

proof

assume not 1 c= c ; :: thesis: contradiction
then c in {0} by CARD_1:49, ORDINAL1:16;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

hence the edgeless _Graph is c -tcolorable by Th161, Th165; :: thesis: verum