:: deftheorem Def30 defines GraphMeet GLIB_014:def 30 :
for G1, G2 being _Graph
for b₃ being Subgraph of G1 holds
( ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 implies ( b₃ is GraphMeet of G1,G2 iff ex S being GraphMeetSet st
( S = {G1,G2} & b₃ is GraphMeet of S ) ) ) & ( ( not G1 tolerates G2 or not the_Vertices_of G1 meets the_Vertices_of G2 ) implies ( b₃ is GraphMeet of G1,G2 iff b₃ == G1 ) ) );