for G, G1, G2, G3 being Graph st G1 c= G3 & G2 c= G3 & G is_sum_of G1,G2 holds
G c= G3