:: deftheorem Def3 defines finite-vcolorable GLCOLO00:def 3 :
for G being _Graph holds
( G is finite-vcolorable iff ex n being Nat st G is n -vcolorable );