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