theorem Th91: :: GLIBPRE1:90

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 total holds
(F _E) .: (G1 .edgesBetween (X,Y)) c= G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))