:: deftheorem defines the_Edges_of GLIB_000:def 7 :
for G being GraphStruct holds the_Edges_of G = G . EdgeSelector;