theorem :: GLIB_000:111

for G being simple _Graph
for v being Vertex of G holds v .degree() = card (v .allNeighbors())