:: deftheorem Def13 defines addAdjVertex GLIB_006:def 13 :
for G being _Graph
for v1 being Vertex of G
for e, v2 being object
for b₅ being Supergraph of G holds
( ( not v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b₅ is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b₅ = (the_Vertices_of G) \/ {v2} & 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) ) ) ) & ( ( v2 in the_Vertices_of G or e in the_Edges_of G ) implies ( b₅ is addAdjVertex of G,v1,e,v2 iff b₅ == G ) ) );