:: deftheorem defines id GLIB_010:def 9 :
for G being _Graph holds id G = [(id (the_Vertices_of G)),(id (the_Edges_of G))];