theorem :: GLUNIR00:58

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