:: deftheorem defines -correct FOMODEL2:def 44 :
for S being Language
for X being set holds
( X is S -correct iff for U being non empty set
for I being Element of U -InterpretersOf S
for x being b₄ -satisfied set
for phi being wff string of S st [x,phi] in X holds
I -TruthEval phi = 1 );