let G be _Graph; :: thesis: for c being Cardinal
for H being Subgraph of G st G is c -vcolorable holds
H is c -vcolorable
let c be Cardinal; :: thesis: for H being Subgraph of G st G is c -vcolorable holds
H is c -vcolorable
let H be Subgraph of G; :: thesis: ( G is c -vcolorable implies H is c -vcolorable )
assume G is c -vcolorable ; :: thesis: H is c -vcolorable
then consider f being VColoring of G such that
A1: ( f is proper & card (rng f) c= c ) ;
reconsider f9 = f | (the_Vertices_of H) as VColoring of H by Th3;
card (rng f9) c= card (rng f) by RELAT_1:70, CARD_1:11;
then card (rng f9) c= c by A1, XBOOLE_1:1;
hence H is c -vcolorable by A1, Th15; :: thesis: verum