theorem Th50: :: GLIB_013:50
for G being _Graph
for c being Cardinal st ex v being Vertex of G st
( v .outDegree() = c & ( for w being Vertex of G holds w .outDegree() c= v .outDegree() ) ) holds
G .supOutDegree() = c