let G1, G2, G9 be _Graph; :: thesis: for G being GraphMeet of G1,G2 holds
( G9 is GraphMeet of G1,G2 iff G == G9 )
let G be GraphMeet of G1,G2; :: thesis: ( G9 is GraphMeet of G1,G2 iff G == G9 )

hereby :: thesis: ( G == G9 implies G9 is GraphMeet of G1,G2 )

assume A1: G9 is GraphMeet of G1,G2 ; :: thesis: G == G9

per cases ( ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 ) or not G1 tolerates G2 or not the_Vertices_of G1 meets the_Vertices_of G2 ) ;

suppose A2: ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 ) ; :: thesis: G == G9

then consider S being GraphMeetSet such that
A3: ( S = {G1,G2} & G is GraphMeet of S ) by Def30;
consider S9 being GraphMeetSet such that
A4: ( S9 = {G1,G2} & G9 is GraphMeet of S9 ) by A1, A2, Def30;
thus G == G9 by A3, A4, Th38; :: thesis: verum

end;

suppose ( not G1 tolerates G2 or not the_Vertices_of G1 meets the_Vertices_of G2 ) ; :: thesis: G == G9

then ( G == G1 & G9 == G1 ) by A1, Def30;
hence G == G9 by GLIB_000:85; :: thesis: verum

end;

end;

end;

assume A5: G == G9 ; :: thesis: G9 is GraphMeet of G1,G2

per cases ( ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 ) or not G1 tolerates G2 or not the_Vertices_of G1 meets the_Vertices_of G2 ) ;

suppose A6: ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 ) ; :: thesis: G9 is GraphMeet of G1,G2

then consider S being GraphMeetSet such that
A7: ( S = {G1,G2} & G is GraphMeet of S ) by Def30;
A8: G9 is Subgraph of G1 by A5, GLIB_000:92;
G9 is GraphMeet of S by A5, A7, Th38;
hence G9 is GraphMeet of G1,G2 by A6, A7, A8, Def30; :: thesis: verum

end;

suppose A9: ( not G1 tolerates G2 or not the_Vertices_of G1 meets the_Vertices_of G2 ) ; :: thesis: G9 is GraphMeet of G1,G2

then G == G1 by Def30;
then A10: G9 == G1 by A5, GLIB_000:85;
then G9 is Subgraph of G1 by GLIB_006:58;
hence G9 is GraphMeet of G1,G2 by A9, A10, Def30; :: thesis: verum

end;

end;