theorem Th48: :: GLIB_013:48

for G being _Graph
for c being Cardinal st ex v being Vertex of G st
( v .degree() = c & ( for w being Vertex of G holds w .degree() c= v .degree() ) ) holds
G .supDegree() = c