theorem :: GLUNIR00:90

for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E holds the_Edges_of G c= E ;