theorem :: GLIB_013:102

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