set E = TheEqSymbOf S;
set t = the termal string of S;
set phi = (<*(TheEqSymbOf S)*> ^ the termal string of S) ^ the termal string of S;
take (<*(TheEqSymbOf S)*> ^ the termal string of S) ^ the termal string of S ; :: thesis: (<*(TheEqSymbOf S)*> ^ the termal string of S) ^ the termal string of S is X -implied

now :: thesis: for U being non empty set
for I being Element of U -InterpretersOf S st X is I -satisfied holds
I -TruthEval ((<*(TheEqSymbOf S)*> ^ the termal string of S) ^ the termal string of S) = 1

let U be non empty set ; :: thesis: for I being Element of U -InterpretersOf S st X is I -satisfied holds
I -TruthEval ((<*(TheEqSymbOf S)*> ^ the termal string of S) ^ the termal string of S) = 1
set II = U -InterpretersOf S;
let I be Element of U -InterpretersOf S; :: thesis: ( X is I -satisfied implies I -TruthEval ((<*(TheEqSymbOf S)*> ^ the termal string of S) ^ the termal string of S) = 1 )
assume X is I -satisfied ; :: thesis: I -TruthEval ((<*(TheEqSymbOf S)*> ^ the termal string of S) ^ the termal string of S) = 1
set TE = I -TermEval ;
(I -TermEval) . the termal string of S = (I -TermEval) . the termal string of S ;
hence I -TruthEval ((<*(TheEqSymbOf S)*> ^ the termal string of S) ^ the termal string of S) = 1 by Lm54; :: thesis: verum

end;

hence (<*(TheEqSymbOf S)*> ^ the termal string of S) ^ the termal string of S is X -implied ; :: thesis: verum