let G1, G2 be _Graph; :: thesis: ( G2 is Subgraph of G1 iff G1 is Supergraph of G2 )
thus ( G2 is Subgraph of G1 implies G1 is Supergraph of G2 ) :: thesis: ( G1 is Supergraph of G2 implies G2 is Subgraph of G1 )

proof

assume G2 is Subgraph of G1 ; :: thesis: G1 is Supergraph of G2
then ( the_Vertices_of G2 c= the_Vertices_of G1 & the_Edges_of G2 c= the_Edges_of G1 & ( 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 GLIB_000:def 32;
hence G1 is Supergraph of G2 by Def9; :: thesis: verum

end;

assume G1 is Supergraph of G2 ; :: thesis: G2 is Subgraph of G1
then ( the_Vertices_of G2 c= the_Vertices_of G1 & the_Edges_of G2 c= the_Edges_of G1 & ( 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 Def9;
hence G2 is Subgraph of G1 by GLIB_000:def 32; :: thesis: verum