theorem :: GLIB_013:54

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is onto & F is semi-Dcontinuous & dom (F _V) = the_Vertices_of G1 holds
G2 .minDegree() c= G1 .minDegree()