:: deftheorem defines with_max_degree GLIB_013:def 18 :
for G being _Graph
for v being Vertex of G holds
( v is with_max_degree iff v .degree() = G .supDegree() );