for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for V being set holds (F _E) .: (G1 .edgesBetween V) c= G2 .edgesBetween ((F _V) .: V)