theorem :: GLUNIR00:98

for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E
for v being Vertex of G holds Im (E,v) = v .allNeighbors()