:: deftheorem defines operational FOMODEL1:def 12 :
for S being Language-like holds
( S is operational iff not OpSymbolsOf S is empty );