let S be GraphMeetSet; :: thesis: for G being GraphMeet of S
for G9 being _Graph holds
( G9 is GraphMeet of S iff G == G9 )
let G be GraphMeet of S; :: thesis: for G9 being _Graph holds
( G9 is GraphMeet of S iff G == G9 )
let G9 be _Graph; :: thesis: ( G9 is GraphMeet of S iff G == G9 )
A1: ( the_Vertices_of G = meet (the_Vertices_of S) & the_Edges_of G = meet (the_Edges_of S) & the_Source_of G = meet (the_Source_of S) & the_Target_of G = meet (the_Target_of S) ) by Def29;

hereby :: thesis: ( G == G9 implies G9 is GraphMeet of S )

assume G9 is GraphMeet of S ; :: thesis: G == G9
then ( the_Vertices_of G9 = meet (the_Vertices_of S) & the_Edges_of G9 = meet (the_Edges_of S) & the_Source_of G9 = meet (the_Source_of S) & the_Target_of G9 = meet (the_Target_of S) ) by Def29;
hence G == G9 by A1, GLIB_000:def 34; :: thesis: verum

end;

assume G == G9 ; :: thesis: G9 is GraphMeet of S
then ( the_Vertices_of G = the_Vertices_of G9 & the_Edges_of G = the_Edges_of G9 & the_Source_of G = the_Source_of G9 & the_Target_of G = the_Target_of G9 ) by GLIB_000:def 34;
hence G9 is GraphMeet of S by A1, Def29; :: thesis: verum