let G1, G2, G9 be _Graph; :: thesis: for G being GraphUnion of G1,G2 holds
( G9 is GraphUnion of G1,G2 iff G == G9 )
let G be GraphUnion of G1,G2; :: thesis: ( G9 is GraphUnion of G1,G2 iff G == G9 )

hereby :: thesis: ( G == G9 implies G9 is GraphUnion of G1,G2 )

assume A1: G9 is GraphUnion of G1,G2 ; :: thesis: G == G9

per cases ( G1 tolerates G2 or not G1 tolerates G2 ) ;

suppose A2: G1 tolerates G2 ; :: thesis: G == G9

then consider S being GraphUnionSet such that
A3: ( S = {G1,G2} & G is GraphUnion of S ) by Def26;
consider S9 being GraphUnionSet such that
A4: ( S9 = {G1,G2} & G9 is GraphUnion of S9 ) by A1, A2, Def26;
thus G == G9 by A3, A4, Th22; :: thesis: verum

end;

suppose not G1 tolerates G2 ; :: thesis: G == G9

then ( G == G1 & G9 == G1 ) by A1, Def26;
hence G == G9 by GLIB_000:85; :: thesis: verum

end;

end;

end;

assume A5: G == G9 ; :: thesis: G9 is GraphUnion of G1,G2

per cases ( G1 tolerates G2 or not G1 tolerates G2 ) ;

suppose A6: G1 tolerates G2 ; :: thesis: G9 is GraphUnion of G1,G2

then consider S being GraphUnionSet such that
A7: ( S = {G1,G2} & G is GraphUnion of S ) by Def26;
A8: G9 is Supergraph of G1 by A5, GLIB_009:40;
G9 is GraphUnion of S by A5, A7, Th22;
hence G9 is GraphUnion of G1,G2 by A6, A7, A8, Def26; :: thesis: verum

end;

suppose A9: not G1 tolerates G2 ; :: thesis: G9 is GraphUnion of G1,G2

then G == G1 by Def26;
then A10: G9 == G1 by A5, GLIB_000:85;
then G9 is Supergraph of G1 by GLIB_006:58;
hence G9 is GraphUnion of G1,G2 by A9, A10, Def26; :: thesis: verum

end;

end;