theorem Th94: :: GLIBPRE0:88

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is directed & F is weak_SG-embedding holds
( v .inDegree() c= ((F _V) /. v) .inDegree() & v .outDegree() c= ((F _V) /. v) .outDegree() )