let G be strict Graph; :: thesis: G is_sum_of G,G
A1: G = G \/ G by Th7;
thus G is_sum_of G,G by A1, Def4; :: thesis: verum