theorem Th41: :: GRAPH_3:41

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