theorem :: GLUNIR00:11

for G being _Graph holds card (VertexDomRel G) c= G .size()