:: deftheorem Def12 defines with_max_degree GLIB_013:def 12 :
for G being _Graph holds
( G is with_max_degree iff ex v being Vertex of G st
for w being Vertex of G holds w .degree() c= v .degree() );