theorem :: GLIB_013:89

for G being locally-finite with_max_out_degree _Graph
for n being Nat holds
( G .maxOutDegree() = n iff ex v being Vertex of G st
( v .outDegree() = n & ( for w being Vertex of G holds w .outDegree() <= v .outDegree() ) ) )