for e being set
for G being Graph
for v1, v2 being Vertex of G st e in the carrier' of G holds
( the Source of (AddNewEdge (v1,v2)) . e = the Source of G . e & the Target of (AddNewEdge (v1,v2)) . e = the Target of G . e )