let G1, G2 be _Graph; :: thesis: for c being Cardinal
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & G2 is c -ecolorable holds
G1 is c -ecolorable
let c be Cardinal; :: thesis: for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & G2 is c -ecolorable holds
G1 is c -ecolorable
let F be PGraphMapping of G1,G2; :: thesis: ( F is weak_SG-embedding & G2 is c -ecolorable implies G1 is c -ecolorable )
assume A1: ( F is weak_SG-embedding & G2 is c -ecolorable ) ; :: thesis: G1 is c -ecolorable
then consider g2 being proper EColoring of G2 such that
A2: card (rng g2) c= c ;
reconsider g1 = g2 * (F _E) as EColoring of G1 by A1, Th84;
A3: g1 is proper by A1, Th98;
card (rng g1) c= card (rng g2) by RELAT_1:26, CARD_1:11;
hence G1 is c -ecolorable by A2, A3, XBOOLE_1:1; :: thesis: verum