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