:: deftheorem Def16 defines operational FOMODEL1:def 16 :
for S being Language-like
for s being Element of S holds
( s is operational iff s in OpSymbolsOf S );