:: deftheorem Def28 defines -prefix FOMODEL1:def 28 :
for S being Language
for X being set holds
( X is S -prefix iff X is AllSymbolsOf S -prefix );