theorem Th3: :: GLIB_008:3

for G being non-Dmulti _Graph
for v being Vertex of G holds v .inDegree() = card (v .inNeighbors())