:: deftheorem defines is_sum_of GRAPH_1:def 6 :
for G, G1, G2 being Graph holds
( G is_sum_of G1,G2 iff ( the Target of G1 tolerates the Target of G2 & the Source of G1 tolerates the Source of G2 & MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2 ) );