hereby :: thesis: ( not G1 tolerates G2 implies ex b1 being Supergraph of G1 st b1 == G1 )
assume G1 tolerates G2 ; :: thesis: ex G being Supergraph of G1 ex S being GraphUnionSet st
( S = {G1,G2} & G is GraphUnion of S )
then reconsider S = {G1,G2} as GraphUnionSet by Th19;
set G = the GraphUnion of S;
G1 in S by TARSKI:def 2;
then G1 is Subgraph of the GraphUnion of S by Th21;
then reconsider G = the GraphUnion of S as Supergraph of G1 by GLIB_006:57;
take G = G; :: thesis: ex S being GraphUnionSet st
( S = {G1,G2} & G is GraphUnion of S )
take S = S; :: thesis: ( S = {G1,G2} & G is GraphUnion of S )
thus ( S = {G1,G2} & G is GraphUnion of S ) ; :: thesis: verum
end;
assume not G1 tolerates G2 ; :: thesis: ex b1 being Supergraph of G1 st b1 == G1
reconsider G = G1 as Supergraph of G1 by GLIB_006:61;
take G ; :: thesis: G == G1
thus G == G1 ; :: thesis: verum