let G1, G2 be Graph; :: thesis: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 implies ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 ) )
assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; :: thesis: ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 )
A2: G1 \/ G2 is_sum_of G1,G2 by A1, Def4;
thus ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 ) by A2, Th18; :: thesis: verum