set E1 = the RepDEdgeSelection of G1;
set E2 = the RepDEdgeSelection of G2;
consider F being directed PGraphMapping of G1,G2 such that
A1: ( F _V = f & dom (F _E) = the RepDEdgeSelection of G1 /\ (G1 .edgesBetween (dom f)) & rng (F _E) c= the RepDEdgeSelection of G2 /\ (G2 .edgesBetween (rng f)) ) by Th29;
take F ; :: thesis: ( F _V = f & dom (F _E) = G1 .edgesBetween (dom f) & rng (F _E) c= G2 .edgesBetween (rng f) )
thus F _V = f by A1; :: thesis: ( dom (F _E) = G1 .edgesBetween (dom f) & rng (F _E) c= G2 .edgesBetween (rng f) )
A2: ( the RepDEdgeSelection of G1 = the_Edges_of G1 & the RepDEdgeSelection of G2 = the_Edges_of G2 ) by GLIB_009:76;
hence dom (F _E) = G1 .edgesBetween (dom f) by A1, XBOOLE_1:28; :: thesis: rng (F _E) c= G2 .edgesBetween (rng f)
thus rng (F _E) c= G2 .edgesBetween (rng f) by A1, A2, XBOOLE_1:28; :: thesis: verum