for G being _Graph st G is with_max_in_degree holds
ex v being Vertex of G st
( v .inDegree() = G .supInDegree() & ( for w being Vertex of G holds w .inDegree() c= v .inDegree() ) )