:: deftheorem defines the_Vertices_of GLIB_014:def 18 :
for S being non empty Graph-membered set holds the_Vertices_of S = { (the_Vertices_of G) where G is Element of S : verum } ;