theorem :: GLIB_013:43

for G being _Graph holds G .minDegree() c= G .supDegree() by SETFAM_1:2;