theorem :: GLIB_010:87

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for X being Subset of (the_Vertices_of G1) st F is isomorphism holds
card (G1 .edgesBetween X) = card (G2 .edgesBetween ((F _V) .: X))