theorem Th66: :: GLIB_016:66

for G being _finite _Graph
for v being Denumeration of (the_Vertices_of G) holds 2 * (G .size()) = Sum ((G .degreeMap()) * v)