:: deftheorem Def10 defines addVertices GLIB_006:def 10 :
for G being _Graph
for V being set
for b₃ being Supergraph of G holds
( b₃ is addVertices of G,V iff ( the_Vertices_of b₃ = (the_Vertices_of G) \/ V & the_Edges_of b₃ = the_Edges_of G & the_Source_of b₃ = the_Source_of G & the_Target_of b₃ = the_Target_of G ) );