:: deftheorem Def27 defines GraphSum GLIB_015:def 27 :
for F being non empty Graph-yielding Function
for b₂ being _Graph holds
( b₂ is GraphSum of F iff ex G9 being GraphUnion of rng (canGFDistinction F) st b₂ is G9 -Disomorphic );