let G be _Graph; :: thesis: for c being Cardinal
for H being Subgraph of G st G is c -ecolorable holds
H is c -ecolorable
let c be Cardinal; :: thesis: for H being Subgraph of G st G is c -ecolorable holds
H is c -ecolorable
let H be Subgraph of G; :: thesis: ( G is c -ecolorable implies H is c -ecolorable )
assume G is c -ecolorable ; :: thesis: H is c -ecolorable
then consider g1 being proper EColoring of G such that
A1: card (rng g1) c= c ;
reconsider g2 = g1 | (the_Edges_of H) as EColoring of H by Th78;
reconsider g2 = g2 as proper EColoring of H by Th89;
card (rng g2) c= card (rng g1) by RELAT_1:70, CARD_1:11;
hence H is c -ecolorable by A1, XBOOLE_1:1; :: thesis: verum