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 )

thus ( I -TruthEval phi = 1 implies {phi} is I -satisfied ) by TARSKI:def 1; :: thesis: ( {phi} is I -satisfied implies I -TruthEval phi = 1 )

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 Def41; :: thesis: verum

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 )

thus ( I -TruthEval phi = 1 implies {phi} is I -satisfied ) by TARSKI:def 1; :: thesis: ( {phi} is I -satisfied implies I -TruthEval phi = 1 )

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 Def41; :: thesis: verum