theorem :: GLIB_013:103

for G being _Graph
for n being Nat st ( for v being Vertex of G holds v .outDegree() c= n ) holds
G is with_max_out_degree