theorem :: GLIB_013:94

for G being _Graph
for v, w being Vertex of G st w is with_max_degree holds
v .degree() c= w .degree()