theorem Th87: :: GLIBPRE0:81

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