let G2, G3 be _Graph; :: thesis: for G1 being Supergraph of G3 st G1 == G2 holds
G2 is Supergraph of G3
let G1 be Supergraph of G3; :: thesis: ( G1 == G2 implies G2 is Supergraph of G3 )
assume G1 == G2 ; :: thesis: G2 is Supergraph of G3
then A1: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) by GLIB_000:def 34;
( the_Vertices_of G3 c= the_Vertices_of G1 & the_Edges_of G3 c= the_Edges_of G1 & ( for e being set st e in the_Edges_of G3 holds
( (the_Source_of G3) . e = (the_Source_of G1) . e & (the_Target_of G3) . e = (the_Target_of G1) . e ) ) ) by GLIB_006:def 9;
hence G2 is Supergraph of G3 by A1, GLIB_006:def 9; :: thesis: verum