set G = the Element of S;
the_Vertices_of the Element of S in the_Vertices_of S ;
hence not the_Vertices_of S is empty ; :: thesis: verum