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