:: deftheorem defines LettersOf FOMODEL1:def 2 :
for S being Language-like holds LettersOf S = the adicity of S " {0};