theorem :: GLUNIR00:29

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