theorem Th34: :: GRAPH_3:34

for G being Graph
for v1, v2 being Vertex of G holds
( the carrier' of G in the carrier' of (AddNewEdge (v1,v2)) & the carrier' of G = the carrier' of (AddNewEdge (v1,v2)) \ { the carrier' of G} & the Source of (AddNewEdge (v1,v2)) . the carrier' of G = v1 & the Target of (AddNewEdge (v1,v2)) . the carrier' of G = v2 )