set SS = AllSymbolsOf S;
set A = AllTermsOf S;

now :: thesis: for x being object st x in AllTermsOf S holds
x in ((AllSymbolsOf S) *) \ {{}}

let x be object ; :: thesis: ( x in AllTermsOf S implies x in ((AllSymbolsOf S) *) \ {{}} )
assume A1: x in AllTermsOf S ; :: thesis: x in ((AllSymbolsOf S) *) \ {{}}
then reconsider t = x as Element of AllTermsOf S ;
( not x in {{}} & x in (AllSymbolsOf S) * ) by A1;
hence x in ((AllSymbolsOf S) *) \ {{}} by XBOOLE_0:def 5; :: thesis: verum

end;

hence AllTermsOf S is Element of bool (((AllSymbolsOf S) *) \ {{}}) by TARSKI:def 3; :: thesis: verum