:: deftheorem Def14 defines -TruthEval FOMODEL2:def 15 :
for S being Language
for U being non empty set
for b₃ being Function of [:(U -InterpretersOf S),(AtomicFormulasOf S):],BOOLEAN holds
( b₃ = S -TruthEval U iff for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds b₃ . (I,phi) = I -AtomicEval phi );