theorem Th88: :: GLUNIR00:88

for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E
for v, w being object holds
( [v,w] in E iff ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G ) )