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