set FF = AllFormulasOf S;
set SS = AllSymbolsOf S;
set IT = ((AllSymbolsOf S) *) \ {{}};

now

let x be set ; :: thesis: ( x in AllFormulasOf S implies x in ((AllSymbolsOf S) *) \ {{}} )
assume x in AllFormulasOf S ; :: thesis: x in ((AllSymbolsOf S) *) \ {{}}
then consider phi being string of S such that
C0: ( x = phi & ex m being Nat st phi is m -wff ) ;
thus x in ((AllSymbolsOf S) *) \ {{}} by C0; :: thesis: verum

end;

hence AllFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}}) by TARSKI:def 3; :: thesis: verum