:: deftheorem Def25 defines GraphUnion GLIB_014:def 25 :
for S being GraphUnionSet
for b₂ being _Graph holds
( b₂ is GraphUnion of S iff ( the_Vertices_of b₂ = union (the_Vertices_of S) & the_Edges_of b₂ = union (the_Edges_of S) & the_Source_of b₂ = union (the_Source_of S) & the_Target_of b₂ = union (the_Target_of S) ) );