:: deftheorem Def7 defines finite-ecolorable GLCOLO00:def 7 :
for G being _Graph holds
( G is finite-ecolorable iff ex n being Nat st G is n -ecolorable );