theorem :: GLUNIR00:60

for G being _Graph
for v being object
for V being Subset of (the_Vertices_of G)
for H being addAdjVertexAll of G,v,V st not v in the_Vertices_of G holds
VertexAdjSymRel H = ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:]