now :: thesis: for U being non empty set
for I being Element of U -InterpretersOf S st X is I -satisfied holds
I -TruthEval (xnot (xnot phi)) = 1

let U be non empty set ; :: thesis: for I being Element of U -InterpretersOf S st X is I -satisfied holds
I -TruthEval (xnot (xnot phi)) = 1
set II = U -InterpretersOf S;
let I be Element of U -InterpretersOf S; :: thesis: ( X is I -satisfied implies I -TruthEval (xnot (xnot phi)) = 1 )
set v = I -TruthEval phi;
set phi1 = xnot phi;
set phi2 = xnot (xnot phi);
set v1 = I -TruthEval (xnot phi);
set v2 = I -TruthEval (xnot (xnot phi));
( ('not' (I -TruthEval phi)) \+\ (I -TruthEval (xnot phi)) = {} & ('not' (I -TruthEval (xnot phi))) \+\ (I -TruthEval (xnot (xnot phi))) = {} ) ;
then A1: ( I -TruthEval (xnot phi) = 'not' (I -TruthEval phi) & I -TruthEval (xnot (xnot phi)) = 'not' (I -TruthEval (xnot phi)) ) by FOMODEL0:29;
assume X is I -satisfied ; :: thesis: I -TruthEval (xnot (xnot phi)) = 1
hence I -TruthEval (xnot (xnot phi)) = 1 by A1, FOMODEL2:def 45; :: thesis: verum

end;

hence for b₁ being wff string of S st b₁ = xnot (xnot phi) holds
b₁ is X -implied ; :: thesis: verum