assume ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 ) ; :: thesis:
then reconsider S = {G1,G2} as GraphMeetSet by Th35;
set G = the GraphMeet of S;
G1 in S by TARSKI:def 2;
then G1 is Supergraph of the GraphMeet of S by Th37;
then reconsider G = the GraphMeet of S as Subgraph of G1 by GLIB_006:57;
take G = G; :: thesis:
take S = S; :: thesis:
thus ( S = {G1,G2} & G is GraphMeet of S ) ; :: thesis:

end;