theorem :: FOMODEL1:6

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