let G, H be _Graph; :: thesis: ( G is GraphUnion of {H} iff G == H )

hereby :: thesis: ( G == H implies G is GraphUnion of {H} )

assume G is GraphUnion of {H} ; :: thesis: G == H
then ( the_Vertices_of G = union (the_Vertices_of {H}) & the_Edges_of G = union (the_Edges_of {H}) & the_Source_of G = union (the_Source_of {H}) & the_Target_of G = union (the_Target_of {H}) ) by Def25;
then ( the_Vertices_of G = union {(the_Vertices_of H)} & the_Edges_of G = union {(the_Edges_of H)} & the_Source_of G = union {(the_Source_of H)} & the_Target_of G = union {(the_Target_of H)} ) by Th5;
then ( the_Vertices_of G = the_Vertices_of H & the_Edges_of G = the_Edges_of H & the_Source_of G = the_Source_of H & the_Target_of G = the_Target_of H ) by ZFMISC_1:25;
hence G == H by GLIB_000:def 34; :: thesis: verum

end;

assume G == H ; :: thesis: G is GraphUnion of {H}
then ( the_Vertices_of G = the_Vertices_of H & the_Edges_of G = the_Edges_of H & the_Source_of G = the_Source_of H & the_Target_of G = the_Target_of H ) by GLIB_000:def 34;
then ( the_Vertices_of G = union {(the_Vertices_of H)} & the_Edges_of G = union {(the_Edges_of H)} & the_Source_of G = union {(the_Source_of H)} & the_Target_of G = union {(the_Target_of H)} ) by ZFMISC_1:25;
then ( the_Vertices_of G = union (the_Vertices_of {H}) & the_Edges_of G = union (the_Edges_of {H}) & the_Source_of G = union (the_Source_of {H}) & the_Target_of G = union (the_Target_of {H}) ) by Th5;
hence G is GraphUnion of {H} by Def25; :: thesis: verum