theorem :: GLUNIR00:43

for G being non-Dmulti _Graph holds G .size() c= card (VertexAdjSymRel G)