let G, H be _Graph; :: thesis: ( G is GraphMeet of {H} iff G == H )
hereby :: thesis: ( G == H implies G is GraphMeet of {H} )
assume G is GraphMeet of {H} ; :: thesis: G == H
then ( the_Vertices_of G = meet (the_Vertices_of {H}) & the_Edges_of G = meet (the_Edges_of {H}) & the_Source_of G = meet (the_Source_of {H}) & the_Target_of G = meet (the_Target_of {H}) ) by Def29;
then ( the_Vertices_of G = meet {(the_Vertices_of H)} & the_Edges_of G = meet {(the_Edges_of H)} & the_Source_of G = meet {(the_Source_of H)} & the_Target_of G = meet {(the_Target_of H)} ) by Th5;
then ( the_Vertices_of G = the_Vertices_of H & the_Edges_of G = the_Edges_of H & the_Source_of G = the_Source_of H & the_Target_of G = the_Target_of H ) by SETFAM_1:10;
hence G == H by GLIB_000:def 34; :: thesis: verum
end;
assume G == H ; :: thesis: G is GraphMeet of {H}
then ( the_Vertices_of G = the_Vertices_of H & the_Edges_of G = the_Edges_of H & the_Source_of G = the_Source_of H & the_Target_of G = the_Target_of H ) by GLIB_000:def 34;
then ( the_Vertices_of G = meet {(the_Vertices_of H)} & the_Edges_of G = meet {(the_Edges_of H)} & the_Source_of G = meet {(the_Source_of H)} & the_Target_of G = meet {(the_Target_of H)} ) by SETFAM_1:10;
then ( the_Vertices_of G = meet (the_Vertices_of {H}) & the_Edges_of G = meet (the_Edges_of {H}) & the_Source_of G = meet (the_Source_of {H}) & the_Target_of G = meet (the_Target_of {H}) ) by Th5;
hence G is GraphMeet of {H} by Def29; :: thesis: verum