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