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

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