theorem Th40: :: GRAPH_3:40

for X being set
for G being Graph
for v1, v2 being Vertex of G
for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v2 & v1 <> v2 holds
Edges_Out (v9,X) = Edges_Out (v2,X)