let G be _Graph; :: thesis: for c being Cardinal st G is c -tcolorable holds
( G is c -vcolorable & G is c -ecolorable )
let c be Cardinal; :: thesis: ( G is c -tcolorable implies ( G is c -vcolorable & G is c -ecolorable ) )
assume G is c -tcolorable ; :: thesis: ( G is c -vcolorable & G is c -ecolorable )
then consider t being TColoring of G such that
A1: ( t is proper & card ((rng (t _V)) \/ (rng (t _E))) c= c ) ;
card (rng (t _V)) c= card ((rng (t _V)) \/ (rng (t _E))) by XBOOLE_1:7, CARD_1:11;
hence G is c -vcolorable by A1, XBOOLE_1:1; :: thesis: G is c -ecolorable
card (rng (t _E)) c= card ((rng (t _V)) \/ (rng (t _E))) by XBOOLE_1:7, CARD_1:11;
hence G is c -ecolorable by A1, XBOOLE_1:1; :: thesis: verum