theorem :: GLIB_000:19

for G being loopless _Graph
for v being Vertex of G holds v .degree() = card (v .edgesInOut())