:: deftheorem defines -cons FOMODEL1:def 25 :
for S being Language holds S -cons = (AllSymbolsOf S) -concatenation ;