theorem Th57: :: GLUNIR00:57

for G being _Graph
for v, w being Vertex of G
for e being object
for H being addEdge of G,v,e,w st not e in the_Edges_of G holds
VertexAdjSymRel H = (VertexAdjSymRel G) \/ {[v,w],[w,v]}