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

now :: thesis: for x being object st x in AllTermsOf S holds
x in (TermSymbolsOf S) *

let x be object ; :: 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) * ; :: 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