let G1, G2 be _Graph; :: thesis: for G being GraphMeet of G1,G2 st G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 holds
G is GraphMeet of G2,G1
let G be GraphMeet of G1,G2; :: thesis: ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 implies G is GraphMeet of G2,G1 )
assume A1: ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 ) ; :: thesis: G is GraphMeet of G2,G1
then consider S being GraphMeetSet such that
A2: ( S = {G1,G2} & G is GraphMeet of S ) by Def30;
A3: G is Subgraph of G2 by A1, Th41;
thus G is GraphMeet of G2,G1 by A1, A2, A3, Def30; :: thesis: verum