:: deftheorem defines .supDegree() GLIB_013:def 6 :
for G being _Graph holds G .supDegree() = union { (v .degree()) where v is Vertex of G : verum } ;