:: deftheorem Def31 defines exal FOMODEL2:def 32 :
for S being Language
for w being string of S holds
( w is exal iff (S -firstChar) . w is literal );