let G1, G2 be _Graph; :: thesis: for G being GraphUnion of G1,G2 st G1 tolerates G2 holds
G is GraphUnion of G2,G1
let G be GraphUnion of G1,G2; :: thesis: ( G1 tolerates G2 implies G is GraphUnion of G2,G1 )
assume A1: G1 tolerates G2 ; :: thesis: G is GraphUnion of G2,G1
then consider S being GraphUnionSet such that
A2: ( S = {G1,G2} & G is GraphUnion of S ) by Def26;
A3: G is Supergraph of G2 by A1, Th26;
thus G is GraphUnion of G2,G1 by A1, A2, A3, Def26; :: thesis: verum