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