let S be Language; :: thesis: 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 )
let U be non empty set ; :: thesis: 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 )
let phi be wff string of S; :: thesis: for I being Element of U -InterpretersOf S holds
( I -TruthEval phi = 1 iff {phi} is I -satisfied )
let I be Element of U -InterpretersOf S; :: thesis: ( I -TruthEval phi = 1 iff {phi} is I -satisfied )

hereby :: thesis: ( {phi} is I -satisfied implies I -TruthEval phi = 1 )

assume A1: I -TruthEval phi = 1 ; :: thesis: {phi} is I -satisfied
for psi being wff string of S st psi in {phi} holds
I -TruthEval psi = 1 by A1, TARSKI:def 1;
hence {phi} is I -satisfied by Def42; :: thesis: verum

end;

assume {phi} is I -satisfied ; :: thesis: I -TruthEval phi = 1
then reconsider X = {phi} as I -satisfied set ;
phi in X by TARSKI:def 1;
hence I -TruthEval phi = 1 by Def42; :: thesis: verum