let G be _Graph; :: thesis: for c being Cardinal
for H being Subgraph of G st G is c -tcolorable holds
H is c -tcolorable
let c be Cardinal; :: thesis: for H being Subgraph of G st G is c -tcolorable holds
H is c -tcolorable
let H be Subgraph of G; :: thesis: ( G is c -tcolorable implies H is c -tcolorable )
assume G is c -tcolorable ; :: thesis: H is c -tcolorable
then consider t being TColoring of G such that
A1: ( t is proper & card ((rng (t _V)) \/ (rng (t _E))) c= c ) ;
reconsider t9 = [((t _V) | (the_Vertices_of H)),((t _E) | (the_Edges_of H))] as TColoring of H by Th138;
( rng (t9 _V) c= rng (t _V) & rng (t9 _E) c= rng (t _E) ) by RELAT_1:70;
then (rng (t9 _V)) \/ (rng (t9 _E)) c= (rng (t _V)) \/ (rng (t _E)) by XBOOLE_1:13;
then card ((rng (t9 _V)) \/ (rng (t9 _E))) c= card ((rng (t _V)) \/ (rng (t _E))) by CARD_1:11;
then card ((rng (t9 _V)) \/ (rng (t9 _E))) c= c by A1, XBOOLE_1:1;
hence H is c -tcolorable by A1, Th151; :: thesis: verum