let S be GraphUnionSet; :: thesis: for G being GraphUnion of S
for G9 being _Graph holds
( G9 is GraphUnion of S iff G == G9 )
let G be GraphUnion of S; :: thesis: for G9 being _Graph holds
( G9 is GraphUnion of S iff G == G9 )
let G9 be _Graph; :: thesis: ( G9 is GraphUnion of S iff G == G9 )
A1: ( the_Vertices_of G = union (the_Vertices_of S) & the_Edges_of G = union (the_Edges_of S) & the_Source_of G = union (the_Source_of S) & the_Target_of G = union (the_Target_of S) ) by Def25;

hereby :: thesis: ( G == G9 implies G9 is GraphUnion of S )

assume G9 is GraphUnion of S ; :: thesis: G == G9
then ( the_Vertices_of G9 = union (the_Vertices_of S) & the_Edges_of G9 = union (the_Edges_of S) & the_Source_of G9 = union (the_Source_of S) & the_Target_of G9 = union (the_Target_of S) ) by Def25;
hence G == G9 by A1, GLIB_000:def 34; :: thesis: verum

end;

assume G == G9 ; :: thesis: G9 is GraphUnion of S
then ( the_Vertices_of G = the_Vertices_of G9 & the_Edges_of G = the_Edges_of G9 & the_Source_of G = the_Source_of G9 & the_Target_of G = the_Target_of G9 ) by GLIB_000:def 34;
hence G9 is GraphUnion of S by A1, Def25; :: thesis: verum