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