theorem Th95: :: GLIB_013:95
for G being _Graph
for v, w being Vertex of G st w is with_max_in_degree holds
v .inDegree() c= w .inDegree()