:: deftheorem Def41 defines -satisfied FOMODEL2:def 42 :
for U being non empty set
for S being Language
for I being Element of U -InterpretersOf S
for X being set holds
( X is I -satisfied iff for phi being wff string of S st phi in X holds
I -TruthEval phi = 1 );