:: deftheorem Def2 defines addAdjVertexToAll GLIB_007:def 2 :
for G being _Graph
for v being object
for V being set
for b₄ being Supergraph of G holds
( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ( b₄ is addAdjVertexToAll of G,v,V iff ( the_Vertices_of b₄ = (the_Vertices_of G) \/ {v} & the_Edges_of b₄ = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of b₄ = (the_Source_of G) +* ((V --> (the_Edges_of G)) --> v) & the_Target_of b₄ = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) ) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ( b₄ is addAdjVertexToAll of G,v,V iff b₄ == G ) ) );