let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & G2 is finite-ecolorable holds
G1 is finite-ecolorable
let F be PGraphMapping of G1,G2; :: thesis: ( F is weak_SG-embedding & G2 is finite-ecolorable implies G1 is finite-ecolorable )
assume A1: ( F is weak_SG-embedding & G2 is finite-ecolorable ) ; :: thesis: G1 is finite-ecolorable
then consider n being Nat such that
A2: G2 is n -ecolorable ;
G1 is n -ecolorable by A1, A2, Th110;
hence G1 is finite-ecolorable ; :: thesis: verum