:: deftheorem Def6 defines -ecolorable GLCOLO00:def 6 :
for c being Cardinal
for G being _Graph holds
( G is c -ecolorable iff ex g being proper EColoring of G st card (rng g) c= c );