:: deftheorem defines with_max_out_degree GLIB_013:def 20 :
for G being _Graph
for v being Vertex of G holds
( v is with_max_out_degree iff v .outDegree() = G .supOutDegree() );