let G1, G2 be _Graph; :: thesis: ( the_Vertices_of G2 c= the_Vertices_of G1 & ( for e, x, y being object st e DJoins x,y,G2 holds
e DJoins x,y,G1 ) implies ( G2 is Subgraph of G1 & G1 is Supergraph of G2 ) )
assume that
A1: the_Vertices_of G2 c= the_Vertices_of G1 and
A2: for e, x, y being object st e DJoins x,y,G2 holds
e DJoins x,y,G1 ; :: thesis: ( G2 is Subgraph of G1 & G1 is Supergraph of G2 )

now :: thesis: for e being object st e in the_Edges_of G2 holds
e in the_Edges_of G1

let e be object ; :: thesis: ( e in the_Edges_of G2 implies e in the_Edges_of G1 )
assume e in the_Edges_of G2 ; :: thesis: e in the_Edges_of G1
then e DJoins (the_Source_of G2) . e,(the_Target_of G2) . e,G1 by A2, GLIB_000:def 14;
hence e in the_Edges_of G1 by GLIB_000:def 14; :: thesis: verum

end;

then A3: the_Edges_of G2 c= the_Edges_of G1 by TARSKI:def 3;

now :: thesis: 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 )

let e be set ; :: thesis: ( e in the_Edges_of G2 implies ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) )
assume e in the_Edges_of G2 ; :: thesis: ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e )
then e DJoins (the_Source_of G2) . e,(the_Target_of G2) . e,G1 by A2, GLIB_000:def 14;
hence ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) by GLIB_000:def 14; :: thesis: verum

end;

hence G2 is Subgraph of G1 by A1, A3, GLIB_000:def 32; :: thesis: G1 is Supergraph of G2
hence G1 is Supergraph of G2 by GLIB_006:57; :: thesis: verum