let G, G1, G2 be Graph; :: thesis: ( G is_sum_of G1,G2 implies G is_sum_of G2,G1 )
assume A1: G is_sum_of G1,G2 ; :: thesis: G is_sum_of G2,G1
A2: the Target of G1 tolerates the Target of G2 by A1, Def4;
A3: ( the Source of G1 tolerates the Source of G2 & MultiGraphStruct(# the carrier of G,the carrier' of G,the Source of G,the Target of G #) = G1 \/ G2 ) by A1, Def4;
A4: the Source of G2 tolerates the Source of G1 by A1, Def4;
A5: MultiGraphStruct(# the carrier of G,the carrier' of G,the Source of G,the Target of G #) = G2 \/ G1 by A2, A3, Th8;
thus G is_sum_of G2,G1 by A2, A4, A5, Def4; :: thesis: verum