:: deftheorem defines the_Vertices_of GLIB_000:def 6 :
for G being GraphStruct holds the_Vertices_of G = G . VertexSelector;