:: deftheorem Def2 defines Interpreter FOMODEL2:def 2 :
for S being Language
for U being non empty set
for s being ofAtomicFormula Element of S
for b₄ being set holds
( ( s is relational implies ( b₄ is Interpreter of s,U iff b₄ is Function of (|.(ar s).| -tuples_on U),BOOLEAN ) ) & ( not s is relational implies ( b₄ is Interpreter of s,U iff b₄ is Function of (|.(ar s).| -tuples_on U),U ) ) );