theorem :: GLIBPRE1:92

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for X, Y being Subset of (the_Vertices_of G1) st F is weak_SG-embedding & F is onto holds
(F _E) .: (G1 .edgesBetween (X,Y)) = G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))