:: deftheorem defines == GLIB_000:def 34 :
for G1, G2 being _Graph holds
( G1 == G2 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 ) );