:: deftheorem Def26 defines GraphUnion GLIB_014:def 26 :
for G1, G2 being _Graph
for b₃ being Supergraph of G1 holds
( ( G1 tolerates G2 implies ( b₃ is GraphUnion of G1,G2 iff ex S being GraphUnionSet st
( S = {G1,G2} & b₃ is GraphUnion of S ) ) ) & ( not G1 tolerates G2 implies ( b₃ is GraphUnion of G1,G2 iff b₃ == G1 ) ) );