theorem Th32: :: GLUNIR00:32

for G being _Graph
for v, w being object holds
( [v,w] in VertexAdjSymRel G iff ex e being object st e Joins v,w,G )