let S be GraphMeetSet; :: thesis: for G being GraphMeet of S
for H being Element of S holds H is Supergraph of G
let G be GraphMeet of S; :: thesis: for H being Element of S holds H is Supergraph of G
let H be Element of S; :: thesis: H is Supergraph of G
the_Vertices_of H in the_Vertices_of S ;
then meet (the_Vertices_of S) c= the_Vertices_of H by SETFAM_1:3;
then A1: the_Vertices_of G c= the_Vertices_of H by Def29;
the_Source_of H in the_Source_of S ;
then meet (the_Source_of S) c= the_Source_of H by SETFAM_1:3;
then A2: the_Source_of G c= the_Source_of H by Def29;
the_Target_of H in the_Target_of S ;
then meet (the_Target_of S) c= the_Target_of H by SETFAM_1:3;
then the_Target_of G c= the_Target_of H by Def29;
hence H is Supergraph of G by A1, A2, GLIB_006:63; :: thesis: verum