theorem Th99: :: GLIB_013:99

for G being _Graph holds
( G is with_max_out_degree iff ex v being Vertex of G st v is with_max_out_degree )