theorem Th97: :: GLIB_013:97

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