theorem Th42: :: GRAPH_3:42

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 & the carrier' of G in X holds
( Edges_In (v9,X) = (Edges_In (v2,X)) \/ { the carrier' of G} & Edges_In (v2,X) misses { the carrier' of G} )