theorem Th41: :: GLIB_000:41

for G1, G2 being _Graph holds
( 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 ) )