:: deftheorem Def35 defines 0wff FOMODEL1:def 35 :
for S being Language
for phi being string of S holds
( phi is 0wff iff ex s being relational Element of S ex V being |.(ar b₃).| -element Element of (AllTermsOf S) * st phi = <*s*> ^ ((S -multiCat) . V) );