theorem :: GLUNIR00:28

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
VertexDomRel H = (VertexDomRel G) \/ {[v,w]}