theorem Th8: :: GLIB_014:8
for S1, S2 being Graph-membered set holds
( the_Vertices_of (S1 \/ S2) = (the_Vertices_of S1) \/ (the_Vertices_of S2) & the_Edges_of (S1 \/ S2) = (the_Edges_of S1) \/ (the_Edges_of S2) & the_Source_of (S1 \/ S2) = (the_Source_of S1) \/ (the_Source_of S2) & the_Target_of (S1 \/ S2) = (the_Target_of S1) \/ (the_Target_of S2) )