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