:: deftheorem Def7 defines AddNewEdge GRAPH_3:def 7 :
for G being Graph
for v1, v2 being Vertex of G
for b₄ being strict Graph holds
( b₄ = AddNewEdge (v1,v2) iff ( the carrier of b₄ = the carrier of G & the carrier' of b₄ = the carrier' of G \/ { the carrier' of G} & the Source of b₄ = the Source of G +* ( the carrier' of G .--> v1) & the Target of b₄ = the Target of G +* ( the carrier' of G .--> v2) ) );