theorem Th57: :: GLIB_013:57

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is directed & F is weak_SG-embedding & rng (F _V) = the_Vertices_of G2 holds
( G1 .minInDegree() c= G2 .minInDegree() & G1 .minOutDegree() c= G2 .minOutDegree() )