:: deftheorem Def11 defines addEdge GLIB_006:def 11 :
for G being _Graph
for v1, e, v2 being object
for b₅ being Supergraph of G holds
( ( v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b₅ is addEdge of G,v1,e,v2 iff ( the_Vertices_of b₅ = the_Vertices_of G & the_Edges_of b₅ = (the_Edges_of G) \/ {e} & the_Source_of b₅ = (the_Source_of G) +* (e .--> v1) & the_Target_of b₅ = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( not v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) implies ( b₅ is addEdge of G,v1,e,v2 iff b₅ == G ) ) );