:: deftheorem defines OwnSymbolsOf FOMODEL1:def 9 :
for S being Language-like holds OwnSymbolsOf S = the carrier of S \ { the ZeroF of S, the OneF of S};