theorem :: GLIB_013:44

for G being _Graph holds G .minInDegree() c= G .supInDegree() by SETFAM_1:2;