theorem Th29: :: GLIB_011:29

for G1, G2 being _Graph
for f being directed PVertexMapping of G1,G2
for E1 being RepDEdgeSelection of G1
for E2 being RepDEdgeSelection of G2 ex F being directed PGraphMapping of G1,G2 st
( F _V = f & dom (F _E) = E1 /\ (G1 .edgesBetween (dom f)) & rng (F _E) c= E2 /\ (G2 .edgesBetween (rng f)) )