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 b1 being set st b1 = (AllTermsOf S) \ ((TermSymbolsOf S) *) holds
b1 is empty ; :: thesis: verum