theorem :: GLIB_000:154

for G being _Graph
for v being Vertex of G st ( for e being object holds not e Joins v,v,G ) holds
card (v .edgesInOut()) = v .degree()