theorem :: GLUNIR00:13

for G being _Graph
for v being Vertex of G holds Im ((VertexDomRel G),v) = v .outNeighbors()