theorem :: GLUNIR00:97

for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E holds
( ( E is total & E is reflexive ) iff G is loopfull )