let G1, G2 be _Graph; :: thesis: ( the_Vertices_of G2 c= the_Vertices_of G1 & the_Source_of G2 c= the_Source_of G1 & the_Target_of G2 c= the_Target_of G1 implies G1 is Supergraph of G2 )
assume that
A1: the_Vertices_of G2 c= the_Vertices_of G1 and
A2: the_Source_of G2 c= the_Source_of G1 and
A3: the_Target_of G2 c= the_Target_of G1 ; :: thesis: G1 is Supergraph of G2
A4: ( dom (the_Source_of G2) = the_Edges_of G2 & dom (the_Target_of G2) = the_Edges_of G2 & dom (the_Source_of G1) = the_Edges_of G1 & dom (the_Target_of G1) = the_Edges_of G1 ) by GLIB_000:4;
A6: the_Edges_of G2 c= the_Edges_of G1 by A3, A4, RELAT_1:11;
for e being set st e in the_Edges_of G2 holds
( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) by A2, A3, A4, GRFUNC_1:2;
hence G1 is Supergraph of G2 by A1, A6, Def9; :: thesis: verum