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