theorem Th25: :: GLIB_014:25

for G1, G2, G being _Graph st G1 tolerates G2 holds
( G is GraphUnion of G1,G2 iff ( the_Vertices_of G = (the_Vertices_of G1) \/ (the_Vertices_of G2) & the_Edges_of G = (the_Edges_of G1) \/ (the_Edges_of G2) & the_Source_of G = (the_Source_of G1) +* (the_Source_of G2) & the_Target_of G = (the_Target_of G1) +* (the_Target_of G2) ) )