:: deftheorem defines .inDegree() GLIB_000:def 42 :
for G being _Graph
for v being Vertex of G holds v .inDegree() = card (v .edgesIn());