for G being _Graph st G is with_max_degree holds
ex v being Vertex of G st
( v .degree() = G .supDegree() & ( for w being Vertex of G holds w .degree() c= v .degree() ) )