theorem :: FOMODEL2:27

for S being Language
for U being non empty set
for phi being wff string of S
for I being Element of U -InterpretersOf S holds
( I -TruthEval phi = 1 iff {phi} is I -satisfied )