for G being _Graph holds
( G is with_max_out_degree iff ex v being Vertex of G st v is with_max_out_degree )