let G1, G2 be _Graph; :: thesis: for G being GraphUnion of G1,G2 st G1 tolerates G2 holds
G is Supergraph of G2
let G be GraphUnion of G1,G2; :: thesis: ( G1 tolerates G2 implies G is Supergraph of G2 )
assume G1 tolerates G2 ; :: thesis: G is Supergraph of G2
then consider S being GraphUnionSet such that
A1: ( S = {G1,G2} & G is GraphUnion of S ) by Def26;
G2 is Element of S by A1, TARSKI:def 2;
then G2 is Subgraph of G by A1, Th21;
hence G is Supergraph of G2 by GLIB_006:57; :: thesis: verum