theorem Th4: :: GLIB_008:4
for G being non-Dmulti _Graph
for v being Vertex of G holds v .outDegree() = card (v .outNeighbors())