:: deftheorem defines AtomicTermsOf FOMODEL1:def 11 :
for S being Language-like holds AtomicTermsOf S = 1 -tuples_on (LettersOf S);