let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
rng ((SG2SGFunc F) | (G1 .allTrees())) c= G2 .allTrees()
let F be PGraphMapping of G1,G2; :: thesis: ( F is weak_SG-embedding implies rng ((SG2SGFunc F) | (G1 .allTrees())) c= G2 .allTrees() )
set f = SG2SGFunc F;
(SG2SGFunc F) | (G1 .allTrees()) = (SG2SGFunc F) | ((G1 .allConnectedSG()) /\ (G1 .allForests())) by Th139
.= ((SG2SGFunc F) | (G1 .allConnectedSG())) /\ ((SG2SGFunc F) | (G1 .allForests())) by RELAT_1:79 ;
then A1: rng ((SG2SGFunc F) | (G1 .allTrees())) c= (rng ((SG2SGFunc F) | (G1 .allConnectedSG()))) /\ (rng ((SG2SGFunc F) | (G1 .allForests()))) by RELAT_1:13;
assume F is weak_SG-embedding ; :: thesis: rng ((SG2SGFunc F) | (G1 .allTrees())) c= G2 .allTrees()
then ( rng ((SG2SGFunc F) | (G1 .allConnectedSG())) c= G2 .allConnectedSG() & rng ((SG2SGFunc F) | (G1 .allForests())) c= G2 .allForests() ) by Th90, Th132;
then (rng ((SG2SGFunc F) | (G1 .allConnectedSG()))) /\ (rng ((SG2SGFunc F) | (G1 .allForests()))) c= (G2 .allConnectedSG()) /\ (G2 .allForests()) by XBOOLE_1:27;
then (rng ((SG2SGFunc F) | (G1 .allConnectedSG()))) /\ (rng ((SG2SGFunc F) | (G1 .allForests()))) c= G2 .allTrees() by Th139;
hence rng ((SG2SGFunc F) | (G1 .allTrees())) c= G2 .allTrees() by A1, XBOOLE_1:1; :: thesis: verum