for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for H being Subgraph of G2 holds (F _E) " (the_Edges_of H) c= G1 .edgesBetween ((F _V) " (the_Vertices_of H))