let G1, G2 be _Graph; :: thesis: ( 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 ) )

hereby :: thesis: ( 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 implies ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) )

assume that
A1: G1 is Subgraph of G2 and
A2: G2 is Subgraph of G1 ; :: thesis: ( 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 )
A3: ( the_Vertices_of G2 c= the_Vertices_of G1 & the_Edges_of G2 c= the_Edges_of G1 ) by A2, Def32;
( the_Vertices_of G1 c= the_Vertices_of G2 & the_Edges_of G1 c= the_Edges_of G2 ) by A1, Def32;
hence A4: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by A3, XBOOLE_0:def 10; :: thesis: ( the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 )
then A5: ( dom (the_Source_of G1) = the_Edges_of G1 & dom (the_Source_of G2) = the_Edges_of G1 ) by FUNCT_2:def 1;
for e being object st e in dom (the_Source_of G1) holds
(the_Source_of G1) . e = (the_Source_of G2) . e by A1, Def32;
hence the_Source_of G1 = the_Source_of G2 by A5, FUNCT_1:2; :: thesis: the_Target_of G1 = the_Target_of G2
A6: ( dom (the_Target_of G1) = the_Edges_of G1 & dom (the_Target_of G2) = the_Edges_of G1 ) by A4, FUNCT_2:def 1;
for e being object st e in dom (the_Target_of G1) holds
(the_Target_of G1) . e = (the_Target_of G2) . e by A1, Def32;
hence the_Target_of G1 = the_Target_of G2 by A6, FUNCT_1:2; :: thesis: verum

end;

assume that
A7: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) and
A8: ( the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) ; :: thesis: ( G1 is Subgraph of G2 & G2 is Subgraph of G1 )
for e being set st e in the_Edges_of G1 holds
( (the_Source_of G1) . e = (the_Source_of G2) . e & (the_Target_of G1) . e = (the_Target_of G2) . e ) by A8;
hence ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) by A7, Def32; :: thesis: verum