theorem Th33: :: GLUNIR00:33

for G being _Graph
for v, w being Vertex of G holds
( [v,w] in VertexAdjSymRel G iff v,w are_adjacent )