:: deftheorem Def13 defines with_max_in_degree GLIB_013:def 13 :
for G being _Graph holds
( G is with_max_in_degree iff ex v being Vertex of G st
for w being Vertex of G holds w .inDegree() c= v .inDegree() );