set TT = AllTermsOf S;
set TS = TermSymbolsOf S;

now

let x be set ; :: thesis: ( x in AllTermsOf S implies x in (TermSymbolsOf S) * )
assume x in AllTermsOf S ; :: thesis: x in (TermSymbolsOf S) *
then reconsider t = x as termal string of S ;
t is FinSequence of TermSymbolsOf S by FOMODEL0:26;
hence x in (TermSymbolsOf S) * by FINSEQ_1:def 11; :: thesis: verum

end;

then AllTermsOf S c= (TermSymbolsOf S) * by TARSKI:def 3;
hence for b₁ being set st b₁ = (AllTermsOf S) \ ((TermSymbolsOf S) *) holds
b₁ is empty ; :: thesis: verum