:: deftheorem Def4 defines addAdjVertexAll GLIB_007:def 4 :
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 addAdjVertexAll of G,v,V iff ( the_Vertices_of b₄ = (the_Vertices_of G) \/ {v} & ( for e being object holds
( not e Joins v,v,b₄ & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,b₄ ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,b₄ holds
e DJoins v1,v2,G ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G & the_Edges_of b₄ = (the_Edges_of G) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,b₄ & ( for e2 being object st e2 Joins v1,v,b₄ holds
e1 = e2 ) ) ) ) ) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ( b₄ is addAdjVertexAll of G,v,V iff b₄ == G ) ) );