let G2 be _Graph; :: thesis: for G1 being Supergraph of G2 st the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of G1 holds
G1 == G2
let G1 be Supergraph of G2; :: thesis: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of G1 implies G1 == G2 )
assume that
A1: the_Vertices_of G2 = the_Vertices_of G1 and
A2: the_Edges_of G2 = the_Edges_of G1 ; :: thesis: G1 == G2
( 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;
then ( the_Source_of G2 = the_Source_of G1 & the_Target_of G2 = the_Target_of G1 ) by A2, Th68, GRFUNC_1:3;
hence G1 == G2 by A1, A2, GLIB_000:def 34; :: thesis: verum