theorem Th38: :: GLIB_013:38

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