LettersOf S c= TermSymbolsOf S by Th1;
hence for b₁ being set st b₁ = TermSymbolsOf S holds
not b₁ is empty ; :: thesis: verum