let G1, G2 be _Graph; :: thesis: ( G1 == G2 iff ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) )
( G1 is Subgraph of G2 & G2 is Subgraph of G1 iff ( 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 Th44;
hence ( G1 == G2 iff ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) ) by Def36; :: thesis: verum