:: deftheorem Def3 defines Interpreter FOMODEL2:def 3 :
for S being Language
for U being non empty set
for b₃ being Function holds
( b₃ is Interpreter of S,U iff for s being own Element of S holds b₃ . s is Interpreter of s,U );