theorem :: GLIB_013:68

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