let G be strict Graph; :: thesis: G is_sum_of G,G
( the Source of G tolerates the Source of G & the Target of G tolerates the Target of G & G = G \/ G ) by Th7;
hence G is_sum_of G,G by Def3; :: thesis: verum