theorem :: GLUNIR00:99

for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E
for X being set holds G .edgesInOut X c= (E | X) \/ (X |` E)