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 {} null S holds
I -TruthEval phi = 1 ;
hence {} null S is S -correct by SeqCorr; :: thesis: verum