set G = the non-empty GeneratorSet of T;
reconsider X = Union the non-empty GeneratorSet of T as VariableSet of T ;
take X ; :: thesis: not X is empty
thus not X is empty ; :: thesis: verum