for S being Language holds AllTermsOf S c= ((AllSymbolsOf S) *) \ {{}} ;