theorem :: GLUNIR00:14

for G being _Graph
for v being Vertex of G holds Coim ((VertexDomRel G),v) = v .inNeighbors()