theorem :: GLIB_016:37

for G being _Graph holds
( G is regular iff G .minDegree() = G .supDegree() )