:: deftheorem Def12 defines finite-tcolorable GLCOLO00:def 12 :
for G being _Graph holds
( G is finite-tcolorable iff ex n being Nat st G is n -tcolorable );