theorem :: GLIB_013:53

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