:: deftheorem defines ExFormulasOf FOMODEL2:def 41 :
for S being Language holds ExFormulasOf S = { phi where phi is string of S : ( phi is wff & phi is exal ) } ;