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 -tcolorable holds
G1 is c -tcolorable
let c be Cardinal; :: thesis: for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & G2 is c -tcolorable holds
G1 is c -tcolorable
let F be PGraphMapping of G1,G2; :: thesis: ( F is weak_SG-embedding & G2 is c -tcolorable implies G1 is c -tcolorable )
assume A1: ( F is weak_SG-embedding & G2 is c -tcolorable ) ; :: thesis: G1 is c -tcolorable
then consider t2 being TColoring of G2 such that
A2: ( t2 is proper & card ((rng (t2 _V)) \/ (rng (t2 _E))) c= c ) ;
reconsider t1 = [((t2 _V) * (F _V)),((t2 _E) * (F _E))] as TColoring of G1 by A1, Th145;
A3: t1 is proper by A1, A2, Th160;
( rng (t1 _V) c= rng (t2 _V) & rng (t1 _E) c= rng (t2 _E) ) by RELAT_1:26;
then (rng (t1 _V)) \/ (rng (t1 _E)) c= (rng (t2 _V)) \/ (rng (t2 _E)) by XBOOLE_1:13;
then card ((rng (t1 _V)) \/ (rng (t1 _E))) c= card ((rng (t2 _V)) \/ (rng (t2 _E))) by CARD_1:11;
hence G1 is c -tcolorable by A2, A3, XBOOLE_1:1; :: thesis: verum