theorem :: GLUNIR00:44

for G being _Graph
for v being Vertex of G holds Im ((VertexAdjSymRel G),v) = v .allNeighbors()