set G = the Element of S;
set v = the Element of the_Vertices_of the Element of S;
( the_Vertices_of the Element of S in the_Vertices_of S & the Element of the_Vertices_of the Element of S in the_Vertices_of the Element of S ) ;
hence not union (the_Vertices_of S) is empty by TARSKI:def 4; :: thesis: verum