:: deftheorem Def25 defines -TruthEval FOMODEL2:def 26 :
for S being Language
for U being non empty set
for I being Element of U -InterpretersOf S
for w being wff string of S
for b₅ being Element of BOOLEAN holds
( b₅ = I -TruthEval w iff for m being Nat st w is m -wff holds
b₅ = ((I,m) -TruthEval) . w );