theorem Th37: :: GLIB_013:37

for G being _Graph
for c being Cardinal holds
( G .minInDegree() = c iff ex v being Vertex of G st
( v .inDegree() = c & ( for w being Vertex of G holds v .inDegree() c= w .inDegree() ) ) )