set FF = AllFormulasOf S;
set SS = AllSymbolsOf S;
set IT = ((AllSymbolsOf S) *) \ {{}};
now :: thesis: for x being object st x in AllFormulasOf S holds
x in ((AllSymbolsOf S) *) \ {{}}
let x be object ; :: 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
A1: ( x = phi & ex m being Nat st phi is m -wff ) ;
thus x in ((AllSymbolsOf S) *) \ {{}} by A1; :: thesis: verum
end;
hence AllFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}}) by TARSKI:def 3; :: thesis: verum