theorem :: GLIB_013:45

for G being _Graph holds G .minOutDegree() c= G .supOutDegree() by SETFAM_1:2;