:: deftheorem defines with_max_in_degree GLIB_013:def 19 :
for G being _Graph
for v being Vertex of G holds
( v is with_max_in_degree iff v .inDegree() = G .supInDegree() );