for G1, G2 being _Graph st the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of G1 & the_Source_of G2 c= the_Source_of G1 & the_Target_of G2 c= the_Target_of G1 holds
G1 == G2