let G1, G2, G be _Graph; :: thesis: ( G1 tolerates G2 implies ( 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) ) ) )
assume A1: G1 tolerates G2 ; :: thesis: ( 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) ) )

hereby :: thesis: ( 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) implies G is GraphUnion of G1,G2 )

assume G is GraphUnion of G1,G2 ; :: thesis: ( 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) )
then consider S being GraphUnionSet such that
A2: ( S = {G1,G2} & G is GraphUnion of S ) by A1, Def26;
thus the_Vertices_of G = union (the_Vertices_of {G1,G2}) by A2, Def25
.= union {(the_Vertices_of G1),(the_Vertices_of G2)} by Th6
.= (the_Vertices_of G1) \/ (the_Vertices_of G2) by ZFMISC_1:75 ; :: thesis: ( 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) )
thus the_Edges_of G = union (the_Edges_of {G1,G2}) by A2, Def25
.= union {(the_Edges_of G1),(the_Edges_of G2)} by Th6
.= (the_Edges_of G1) \/ (the_Edges_of G2) by ZFMISC_1:75 ; :: thesis: ( the_Source_of G = (the_Source_of G1) +* (the_Source_of G2) & the_Target_of G = (the_Target_of G1) +* (the_Target_of G2) )
thus the_Source_of G = union (the_Source_of {G1,G2}) by A2, Def25
.= union {(the_Source_of G1),(the_Source_of G2)} by Th6
.= (the_Source_of G1) \/ (the_Source_of G2) by ZFMISC_1:75
.= (the_Source_of G1) +* (the_Source_of G2) by A1, FUNCT_4:30 ; :: thesis: the_Target_of G = (the_Target_of G1) +* (the_Target_of G2)
thus the_Target_of G = union (the_Target_of {G1,G2}) by A2, Def25
.= union {(the_Target_of G1),(the_Target_of G2)} by Th6
.= (the_Target_of G1) \/ (the_Target_of G2) by ZFMISC_1:75
.= (the_Target_of G1) +* (the_Target_of G2) by A1, FUNCT_4:30 ; :: thesis: verum

end;

assume A3: ( 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) ) ; :: thesis: G is GraphUnion of G1,G2
reconsider S = {G1,G2} as GraphUnionSet by A1, Th19;
A4: the_Vertices_of G1 c= the_Vertices_of G by A3, XBOOLE_1:7;
the_Source_of G = (the_Source_of G1) \/ (the_Source_of G2) by A1, A3, FUNCT_4:30;
then A5: the_Source_of G1 c= the_Source_of G by XBOOLE_1:7;
the_Target_of G = (the_Target_of G1) \/ (the_Target_of G2) by A1, A3, FUNCT_4:30;
then A6: G is Supergraph of G1 by A4, A5, XBOOLE_1:7, GLIB_006:63;
A7: the_Vertices_of G = union {(the_Vertices_of G1),(the_Vertices_of G2)} by A3, ZFMISC_1:75
.= union (the_Vertices_of S) by Th6 ;
A8: the_Edges_of G = union {(the_Edges_of G1),(the_Edges_of G2)} by A3, ZFMISC_1:75
.= union (the_Edges_of S) by Th6 ;
A9: the_Source_of G = (the_Source_of G1) \/ (the_Source_of G2) by A1, A3, FUNCT_4:30
.= union {(the_Source_of G1),(the_Source_of G2)} by ZFMISC_1:75
.= union (the_Source_of S) by Th6 ;
the_Target_of G = (the_Target_of G1) \/ (the_Target_of G2) by A1, A3, FUNCT_4:30
.= union {(the_Target_of G1),(the_Target_of G2)} by ZFMISC_1:75
.= union (the_Target_of S) by Th6 ;
then G is GraphUnion of S by A7, A8, A9, Def25;
hence G is GraphUnion of G1,G2 by A1, A6, Def26; :: thesis: verum