set sub = SubTerms phi0;
set TS = TermSymbolsOf S;
set TT = AllTermsOf S;
(AllTermsOf S) \ ((TermSymbolsOf S) *) = {} ;
then reconsider TTT = AllTermsOf S as non empty Subset of ((TermSymbolsOf S) *) by XBOOLE_1:37;
SubTerms phi0 is TTT -valued ;
hence SubTerms phi0 is (TermSymbolsOf S) * -valued ; :: thesis: verum