theorem Th27: :: GLIB_011:27

for G1, G2 being _Graph
for f being PVertexMapping of G1,G2
for E1 being RepEdgeSelection of G1
for E2 being RepEdgeSelection of G2 ex F being 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)) )