theorem Th86: :: GLIBPRE0:80

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st v in dom (F _V) holds
(F _E) .: (v .edgesInOut()) c= ((F _V) /. v) .edgesInOut()