theorem :: GLIB_013:42
for G being _Graph holds G .minOutDegree() c= G .minDegree()