:: deftheorem defines -tcolorable GLCOLO00:def 11 :
for c being Cardinal
for G being _Graph holds
( G is c -tcolorable iff ex t being TColoring of G st
( t is proper & card ((rng (t _V)) \/ (rng (t _E))) c= c ) );