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