set FF = AllFormulasOf S;

set SS = AllSymbolsOf S;

set IT = ((AllSymbolsOf 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) *) \ {{}}

hence
AllFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}})
by TARSKI:def 3; :: thesis: verumx 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;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