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