for G1, G2, G being _Graph st G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 holds
( G is GraphMeet of G1,G2 iff ( the_Vertices_of G = (the_Vertices_of G1) /\ (the_Vertices_of G2) & the_Edges_of G = (the_Edges_of G1) /\ (the_Edges_of G2) & the_Source_of G = (the_Source_of G1) /\ (the_Source_of G2) & the_Target_of G = (the_Target_of G1) /\ (the_Target_of G2) ) )