:: deftheorem Def28 defines GraphSum GLIB_015:def 28 :
for G1, G2 being _Graph
for b₃ being Supergraph of G1 holds
( b₃ is GraphSum of G1,G2 iff b₃ is GraphSum of <*G1,G2*> );