:: deftheorem defines -vcolorable GLCOLO00:def 2 :
for c being Cardinal
for G being _Graph holds
( G is c -vcolorable iff ex f being VColoring of G st
( f is proper & card (rng f) c= c ) );